##
Course Outline |
||

Week |
Lecture Dates |
Lecture Topic |
Lab Date |
Lab Topic |

1 | Sep 07, 12 | Introduction | Sep 08 | No lab |

2 | Sep 14, 19 | First-order logic - Syntax and Semantics | Sep 15 | Introduction to Coq, Natural Deduction (propositional logic) in Coq |

3 | Sep 21, 26 | First-order logic - Natural Deduction | Sep 22 | Natural Deduction (first-order logic) in Coq |

4 | Sep 28, Oct 03 | First-order logic - Soundness of Natural Deduction | Sep 29 | Test 1 |

5^{*} |
Oct 05, 17 | Introduction of the Programming Logic IMP and Hoare Logic | Oct 06 | Natural number and induction in Coq |

6 | Oct 19, 24 | Programming Language IMP - Syntax and Operational Semantics | Oct 20 | Hoare logic in Coq |

7 | Oct 26, 31 | Programming Language IMP - Hoare Logic | Oct 27 | Test 2 |

8 | Nov 02, 07 | Programming Language IMP - Soundness of Hoare logic | Nov 03 | IHoare logic in Coq |

9 | Nov 09, 14 | Algebraic Specifications - Motivation, Syntax and Semantics | Nov 10 | Hoare logic (lists and pseudo-pointers) in Coq |

10 | Nov 16, 21 | Algebraic Specifications - Homomorphisms, Initial and Terminal Models | Nov 17 | Test 3 |

11 | Nov 23, 28 | Algebraic Specifications - Homomorphisms, Initial and Terminal Models | Nov 24 | Hoare logic (lists and pseudo-pointers) in Coq |

12 | Nov 30, Dec 05 | Selected topics, Review | Dec 01 | Theories and Hoare Logic in Coq |

- The Formal Semantics of Programming Languages: An Introduction, G. Winskel, The MIT Press (1993), ISBN 0-262-23169-7 (hc), 0-262-73103-7 (pb)
- The Design of Well-Structured and Correct Programs, S. Alagic & M.A. Arbib, Springer-Verlag (1978), ISBN 0-387-90299-6
- Fundamentals of Algebraic Specifications 1: Equations and Initial Semantics, H. Ehrig & B. Mahr, Springer-Verlag (1985), ISBN 0-387-13718-1
- Logic in Computer Science, 2nd edition, M. Huth & M. Ryan, Cambridge University Press (2004), ISBN 0-521-54310-X

COSC 4P42 Home Page