This schedule is a living document and subject to change: please check back often.
| # | Day | Date | Module | Title | Assignment due |
|---|---|---|---|---|---|
| 1 | Fri | Jan 9 | Intro | Welcome! | |
| 2 | Tue | Jan 13 | Intro | Calculator language | hw1 (Jan 15) |
| 3 | Fri | Jan 16 | Lambda calculus | Let language | |
| 4 | Tue | Jan 20 | Lambda calculus | Lambda Calculus I | hw2 (Jan 22) |
| 5 | Fri | Jan 23 | Lambda calculus | Lambda Calculus II | |
| 6 | Tue | Jan 27 | Lambda calculus | PL on Paper (operational semantics) | hw3 (Jan 29) |
| 7 | Fri | Jan 30 | Types | Type Safety and Simply-typed Lambda Calculus | |
| 8 | Tue | Feb 3 | Types | Product and Sum Types | |
| 9 | Fri | Feb 6 | Types | Bidirectional typing | |
| 10 | Tue | Feb 10 | Types | Recursive Types | hw4 (Feb 12) |
| 11 | Fri | Feb 13 | Types | Recursion and termination / Type Safety, revisited | |
| 12 | Tue | Feb 17 | Types | Types as Propositions | |
| 13 | Fri | Feb 20 | Types | Polymorphism (System F) | |
| 14 | Tue | Feb 24 | Review | hw5 (Feb 26) | |
| 15 | Fri | Feb 27 | Midterm exam | ||
| 16 | Tue | Mar 3 | (No class: Spring Break) | ||
| 17 | Fri | Mar 6 | (No class: Spring Break) | ||
| 18 | Tue | Mar 10 | Guest lecture (TBD) | ||
| 19 | Fri | Mar 13 | Control | Abstract machines | |
| 20 | Tue | Mar 17 | Control | Exceptions | |
| 21 | Fri | Mar 20 | Control | First-class continuations | |
| 22 | Tue | Mar 24 | Effects | Imperative programming | hw6 (Mar 23) |
| 23 | Fri | Mar 27 | Effects | Monads | |
| 24 | Tue | Mar 31 | Proofs | Programming with dependent types | |
| 25 | Fri | Apr 3 | Proofs | Encoding languages with dependent types | |
| 26 | Tue | Apr 7 | Proofs | Mechanizing metatheory I | |
| 27 | Fri | Apr 10 | Proofs | Mechanizing metatheory II | |
| 28 | Tue | Apr 14 | Proofs | Types as Propositions II: Dependent Types | miniproject (Apr 16) |
| 29 | Fri | Apr 17 | Conclusion | ||
| Mon | Apr 20 | Final exam period | miniproject presentation | ||
| Tue | 28 | Faculty grade deadline 2pm |