Course Outline

Instructor: Michael Winter, Office J323, Office Hours: Mon & Fri, 9:00am - 11:00am, 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 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.

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