COMP 360-1: Computer-Checked Programs and Proofs

Schedule of Lectures

Num Day Date Topics Covered Materials
0 Th 21 Jan Proof Assistants TA notes
1 Tu 26 Jan Propositions as types TA notes, code
2 Th 28 Jan Propositions as types TA notes
3 Tu 2 Feb Agda basics Agda code , TA notes
4 Th 4 Feb Induction; Agda installation handout, solution
5 Tu 9 Feb Agda Basics lab
6 Th 11 Feb Lists handout, solution
7 Tu 16 Feb With handout, solution
8 Th 18 Feb Equality Type code
9 Tu 23 Feb Magic With; Inductive Families; Implicit Arguments handout, solution
10 Th 25 Feb Inductive Families Lab handout, solution
11 Tu 1 Mar Red-black Trees reading, code
12 Th 3 Mar Red-black Trees
13 Tu 22 Mar Regexp reading, see HW6 for code
14 Th 24 Mar Regexp
15 Tu 29 Mar Regexp
16 Th 31 Mar Regexp lab
17 Tu 5 Apr Universes code, library code
18 Th 7 Apr Printf code
19 Tu 12 Apr Explicit Termination Metrics code
20 Th 14 Apr Serialization see HW7
21 Tu 19 Apr Circuits See HW8
22 Th 21 Apr HW7 Review
23 Tu 26 Apr Imperative Programming See HW8
24 Th 28 Apr Compiling to Circuits See HW8
25 Tu 3 May Homotopy type theory