| 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 | |