| Num | Day | Date | Topics Covered | Materials |
|---|---|---|---|---|
| 1 | Tu | 3 Sep | Overview | |
| 2 | Th | 5 Sep | Propositions as types | SML code |
| 3 | Tu | 10 Sep | Props as types II: Quantifiers | |
| 4 | Th | 12 Sep | Agda basics | Agda code |
| 5 | Tu | 17 Sep | Lab 1: Agda Basics | Starter code, Solutions |
| 6 | Th | 19 Sep | Review HW2 | HW2 Solutions |
| 7 | Tu | 24 Sep | Inductive Families | Code for 7 and 8 |
| 8 | Th | 26 Sep | Inductive Families II | Code for 7 and 8 |
| 9 | Tu | 1 Oct | Magic With | Starter Code, Finished Code |
| 10 | Th | 3 Oct | Implicit Arguments, Intrinsic vs. Extrinsic Verification | Starter Code, Finished Code |
| 11 | Tu | 8 Oct | Red-Black Trees I | Notes PDF, Library Code, BlackHeight Code |
| 13 | Th | 10 Oct | Red-Black Trees II | Notes PDF, Library Code, BlackHeight Code |
| 13 | Tu | 15 Oct | No class: take-home midterm | |
| 14 | Th | 17 Oct | No class: take-home midterm | |
| 15 | Tu | 22 Oct | No class: Fall break | |
| 16 | Th | 24 Oct | Red-black trees III: Well-red | |
| 17 | Tu | 29 Oct | Type-generic programming using universes | |
| 18 | Th | 31 Oct | Type-safe printf | Preliminaries.agda, Lecture Code |
| 19 | Tu | 5 Nov | Type-generic serialization I | Lecture Code |
| 20 | Th | 7 Nov | Type-generic serialization II | Lecture Code |
| 21 | Tu | 12 Nov | Datatype-generic programming | Lecture Code |
| 22 | Th | 14 Nov | Datatype-generic programming II | Lecture Code |
| 23 | Tu | 19 Nov | Introduction to Homotopy Type Theory | The HoTT book, chapters 1 and 2 |
| 24 | Th | 21 Nov | Higher Inductive Types | HoTT book, chapter 6 |
| 25 | Tu | 26 Nov | Homotopy Theory in Type Theory | HoTT book, chapter 8 |
| 26 | Th | 28 Nov | No Class: Thanksgiving | |
| 27 | Tu | 3 Dec | Quotient Types; Git as a HIT | slides |
| 28 | Th | 5 Dec | Final Project Presentations | |