COSC 4P42 Course Outline

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

Calendar description

Course Outline

Week	Lecture Dates	Lecture Topic	Lab Date	Lab Topic
1	Jan 11/13	Introduction		No lab
2	Jan 18/20	First-order logic - Syntax and Semantics	Jan 17	Introduction to Coq, Natural Deduction (propositional logic) in Coq
3	Jan 25/27	First-order logic - Natural Deduction	Jan 24	Natural Deduction (first-order logic) in Coq
4	Feb 01/03	First-order logic - Soundness of Natural Deduction	Jan 31	Test 1
5	Feb 08/10	Introduction of the Programming Logic IMP and Hoare Logic	Feb 07	Natural number and induction in Coq
6	Feb 15/17	Programming Language IMP - Syntax and Operational Semantics	Feb 14	Hoare logic in Coq
7*	Mar 01/03	Programming Language IMP - Hoare Logic	Feb 28	Test 2
8	Mar 08/10	Programming Language IMP - Soundness of Hoare logic	Mar 07	Hoare logic in Coq
9	Mar 15/17	Algebraic Specifications - Motivation, Syntax and Semantics	Mar 14	Hoare logic (lists and pseudo-pointers) in Coq
10	Mar 22/24	Algebraic Specifications - Homomorphisms, Initial and Terminal Models	Mar 21	Test 3
11	Mar 29/31	Algebraic Specifications - Homomorphisms, Initial and Terminal Models	Mar 28	Hoare logic (lists and pseudo-pointers) in Coq
12**	Apr 05/10	Selected topics, Review		No lab

^* Febrary 20-24 is Reading Week, no classes.
^** April 07 is Good Friday, Make up on April 10.

Supplemental Texts

• 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