Course Outline

Instructor: Michael Winter, Office J323, Office J323, Office Hours: Mon & Wed, 10:00am - noon, email:

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

Date Topics
1 Sep 07/12 Introduction, Principle of functional programming and interactive theorem proving
2 Sep 14/19 Functions as proofs, Proofs as functions
3 Sep 21/26 Coq basics
4 Sep 28/Oct 03 Programming in Coq I
5* Oct 05/17 Programming in Coq II
6 Oct 19/24 Verification of functional programs in Coq I, (Test 1)
7 Oct 26/31 Verification of functional programs in Coq II
8 Nov 02/07 Verification of functional programs in Coq III
9 Nov 09/14` Algebraic theories in Coq I
10 Nov 16/21` Algebraic theories in Coq II
11 Nov 23/28 Algebraic theories in Coq III, (Test 2)
12 Nov 30/Dec 05 Further features of Coq, Review
* October 10-14 is Reading Week, no classes.

COSC Home Page
COSC 5V90 Home Page
© M. Winter, 2016