| September 2 | Course Overview | slides video | |
| September 4 | Introduction to Semantics | slides notes video | |
| September 7 | Inductive Definitions | slides notes video | |
| September 9 | Properties and Inductive Proofs | same slides same notes video | |
| September 11 | Inductive Proof and Large-Step Semantics | slides notes video | |
| September 14 | The IMP Language | slides notes video | HW1 due |
| September 16 | IMP Properties | slides notes video | |
| September 18 | More IMP Proofs | same slides same notes whiteboard-1 whiteboard-2 video-1 video-2 | |
| September 21 | Denotational Semantics | slides notes video | HW2 due |
| September 23 | Denotational Semantics Examples | slides notes video | |
| September 25 | Axiomatic Semantics | slides notes video | |
| September 28 | Hoare Logic | slides notes video | HW3 due |
| September 30 | Hoare Logic Examples | slides notes video | |
| October 2 | Weakest Preconditions | slides notes video | |
| October 5 | λ-Calculus | notes video | Take-Home Prelim 1 |
| October 7 | More λ-Calculus and Substitution | slides notes video | |
| October 9 | de Bruijn and Combinators | slides notes video | Project Charter due |
| October 12 | Encodings | slides notes video | |
| October 14 | Mid-semester break | |
| October 16 | Encodings and Fixed-Point Combinators | slides notes video | |
| October 19 | Definitional Translation | slides notes video | HW4 due |
| October 21 | Continuations | slides notes video | |
| October 23 | Types | slides notes video | |
| October 26 | More Types | same slides same notes video | HW5 due |
| October 28 | Proving Type Soundness | slides notes video | |
| October 30 | More Proving Type Soundness | same slides same notes video | |
| November 2 | Normalization | slides notes video | HW6 due |
| November 4 | Advanced Types | slides notes video | |
| November 6 | Polymorphism | slides notes video | |
| November 9 | Type Inference | slides notes video | Take-Home Prelim 2 |
| November 11 | Recursive Types | slides notes video | |
| November 13 | Records and Subtyping | slides notes video | Project Alpha due |
| November 16 | Study days | |
| November 18 | Semi-finals | |
| November 20 | Semi-finals | |
| November 23 | Semi-finals | |
| November 25 | No class (Thanksgiving) | |
| November 27 | No class (Thanksgiving) | |
| November 30 | Existential Types | slides notes video | |
| December 2 | Propositions as Types | slides notes video | |
| December 4 | Dependent Types | notes video code | Project Beta due |
| December 7 | Concurrency | slides video | Homework 7 due |
| December 9 | Probabilistic Semantics | | |
| December 11 | After 4110 (Guest lecture: TAs) | slides video | |
| December 14 | DSLs and Bidirectional Programming | slides video | Homework 8 due |
| December 16 | Victory Lap | slides video | Final Project due |