COSC 5V90 Course Outline

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

Course description

Introduction to the dependently typed functional programming language of Coq as well as its formal language for mathematical definitions and theorems. Introduction to higher-order logic, interactive theorem proving. Development of verified software using the Coq system.

Course Outline

Week	Date	Topics
1	Jan 09/11	Introduction, Principle of functional programming and interactive theorem proving
2	Jan 16/18	Functions as proofs, Proofs as functions
3	Jan 23/25	Coq basics
4	Jan 30, Feb 01	Programming in Coq I
5	Feb 06/08	Programming in Coq II, (Test 1)
6	Feb 13/15	Verification of functional programs in Coq I, (Test 1)
7*	Feb 27, Mar 01	Verification of functional programs in Coq II
8	Mar 06/08	Verification of functional programs in Coq III
9	Mar 13/15	Algebraic theories in Coq I, (Test 2)
10	Mar 20/22	Algebraic theories in Coq II
11	Mar 27/29	Algebraic theories in Coq III
12	Apr 03/05	Further features of Coq, Review

^* February 19-February 23, 2018 is Reading Week, no classes.