| Date | Lecture | Reading | Homework | |||
|---|---|---|---|---|---|---|
| |
||||||
| Th | Jan | 3 | Introduction - Formal syntax | Ch 1, Ch 2 | ||
| |
||||||
| Tu | Jan | 8 | Operational Semantics | Ch 3, Ch 4 | HW 1 out | |
| Th | Jan | 10 | No Class | |||
| |
||||||
| Tu | Jan | 15 | Operational semantics - cont. | Ch 3, Ch 4, Ch 8 | ||
| Th | Jan | 17 | Type systems | Ch 5, Ch 9 | ||
| |
||||||
| Tu | Jan | 22 | Extensions: Let, Pair | Ch 11.5, Ch 11.6 | ||
| Th | Jan | 24 | Normalization | Ch 12 | HW1 due / HW2 out | |
| |
||||||
| Tu | Jan | 29 | Extension: References | CH 13 | ||
| Th | Jan | 31 | Type inference | CH 22 | ||
| |
||||||
| Tu | Feb | 5 | Type inference | CH 22 | ||
| Th | Feb | 7 | Universal Polymorphism | CH 23 | HW2 due / HW3 out | |
| |
||||||
| Tu | Feb | 12 | Subtyping | |||
| Th | Feb | 14 | Subtyping | |||
| |
||||||
| Tu | Feb | 19 | Review | |||
| Th | Feb | 21 | Midterm | HW3 due | ||
| |
||||||
| Tu | Feb | 26 | Break | |||
| Th | Feb | 28 | Break | |||
| |
||||||
| Tu | Mar | 4 | Mechanizing the theory of programming languages | |||
| Th | Mar | 6 | Introduction to logical frameworks | |||
| |
||||||
| Tu | Mar | 11 | Programming with types | |||
| Th | Mar | 13 | Programming with proofs | HW4 out | ||
| |
||||||
| Tu | Mar | 18 | Programming with proofs | |||
| Th | Mar | 20 | Holiday | |||
| |
||||||
| Tu | Mar | 25 | Dependent types | |||
| Th | Mar | 27 | Modal types | HW4 due / HW5 out | ||
| |
||||||
| Tu | Apr | 2 | Programming and HOAS | |||
| Th | Apr | 4 | Programming and HOAS | |||
| |
||||||
| Tu | Apr | 8 | Substructural type systems | |||
| Th | Apr | 10 | Overflow | HW 5 due | ||