COSC 4P42
Course Outline

Instructor: Michael Winter, Office J323, Office Hours: Mon & Fri 9:00am - 11:00am, email: mwinter@brocku.ca


Calendar description

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
* October 09-13 is Reading Week, no classes.

Supplemental Texts


COSC Home Page
COSC 4P42 Home Page
© M. Winter, 2017