| August 27 | Course Overview | slides | |
| August 30 | Introduction to Semantics | slides notes | |
| September 1 | Inductive Definitions | same slides same notes | |
| September 3 | Properties and Inductive Proofs | slides notes | |
| September 6 | Labor Day | |
| September 8 | Inductive Proof | same slides same notes | |
| September 10 | Large-Step Semantics | slides notes | |
| September 13 | The IMP Language | slides notes | A1 due |
| September 15 | IMP Properties | slides notes | |
| September 17 | Denotational Semantics | slides notes | |
| September 20 | Denotational Semantics Examples | slides notes | A2 due |
| September 22 | Axiomatic Semantics | slides notes | |
| September 24 | More Axiomatic Semantics | same slides same notes | |
| September 27 | Hoare Logic | slides notes | A3 due |
| September 29 | Hoare Logic Examples | slides notes | |
| October 1 | Weakest Preconditions | slides notes | |
| October 4 | λ-Calculus | notes | A4 due |
| October 6 | More λ-Calculus and Substitution | slides notes | |
| October 8 | Encodings | slides notes | |
| October 11 | Fall Break | |
| October 13 | Fixed-Point Combinators | slides notes | |
| October 15 | de Bruijn and Combinators | slides notes | |
| October 18 | Preliminary Exam I | |
| October 20 | Definitional Translation | slides notes | |
| October 22 | Continuations | slides notes | |
| October 25 | Types | slides notes | A5 due |
| October 27 | Proving Type Soundness | same slides notes | |
| October 29 | More Soundness | same slides same notes | |
| November 1 | Normalization | slides notes | A6 due |
| November 3 | Advanced Types | slides notes | |
| November 5 | Polymorphism | slides notes | |
| November 8 | More Polymorphism | same slides same notes | A7 due |
| November 10 | Type Inference | slides notes | |
| November 12 | Recursive Types | slides notes | |
| November 15 | Preliminary Exam II | |
| November 17 | Records and Subtyping | slides notes | |
| November 19 | Existential Types | slides notes | |
| November 22 | Propositions as Types | slides notes | A8 due |
| November 24 | No class (Thanksgiving) | |
| November 26 | No class (Thanksgiving) | |
| November 29 | Linear Types | notes | |
| December 1 | Higher-Kinded Types | notes | |
| December 3 | Dependent Types | notes | |
| December 6 | Synthesis | notes | A9 due |
| December 13 | Final Exam, 9:00am, Phillips 101 | |