Lecture materials are available in the lectures/folder of this github repo
| Num | Day | Date | Topics Covered | Materials |
|---|---|---|---|---|
| 1 | Th | 22 Jan | Proof Assistants | slides, notes |
| 2 | Tu | 27 Jan | Propositions as types (And,Implies) | notes |
| 3 | Th | 29 Jan | Propositions as types (Or), Agda Basics | notes |
| 4 | Tu | 3 Feb | Props as types for Forall, Induction | notes |
| 5 | Th | 5 Feb | Props as types for Forall, Induction | notes |
| 6 | Tu | 10 Feb | Existentials, Lists, Linear Search | notes |
| 7 | Th | 12 Feb | Existentials, Lists, Linear Search | notes |
| 8 | Tu | 17 Feb | Regular Expression Matching | notes |
| 9 | Th | 19 Feb | Regular Expression Matching | notes |
| 10 | Tu | 24 Feb | With | notes |
| 11 | Th | 26 Feb | Propositional Equality | notes |
| 12 | Tu | 3 Mar | Inductive Families | notes |
| 13 | Th | 5 Mar | Inductive Families Lab | notes |
| 14 | Tu | 24 Mar | Regular Expressions with Repetitions | See Homework 7 handout. |
| 15 | Th | 26 Mar | Manual Termination Proof in RegExp | See Homework 7 handout. |
| 16 | Tu | 31 Mar | Stack-based RegExp | notes |
| 17 | Th | 2 April | Stack-based RegExp | notes |
| 18 | Tu | 7 April | HW07 help session | |
| 19 | Th | 9 April | Sorted Trees | notes |
| 20 | Tu | 14 April | Sorted Trees and Red-black trees | notes |
| 21 | Th | 16 April | Red-black trees | See Homework 09 handout |
| 22 | Tu | 21 April | Tactics | notes |
| 23 | Th | 23 April | Tactics Lab | |
| 24 | Tu | 28 April | Lab/Homework Session | |
| 25 | Th | 30 April | Lecture: Spaces as Types | |
| 26 | Tu | 5 May | ||
| ...Remaining topics TBA... | ||||
| Tu-Fri | May 12 to 15 | Schedule a 1-on-1 Oral final exam / final homework presentation |
Possible topics for after spring break: