September 2Course Overviewslides video
September 4Introduction to Semanticsslides notes video
September 7Inductive Definitionsslides notes video
September 9Properties and Inductive Proofssame slides same notes video
September 11Inductive Proof and Large-Step Semanticsslides notes video
September 14The IMP Languageslides notes video HW1 due
September 16IMP Propertiesslides notes video
September 18More IMP Proofssame slides same notes whiteboard-1 whiteboard-2 video-1 video-2
September 21Denotational Semanticsslides notes video HW2 due
September 23Denotational Semantics Examplesslides notes video
September 25Axiomatic Semanticsslides notes video
September 28Hoare Logicslides notes video HW3 due
September 30Hoare Logic Examplesslides notes video
October 2Weakest Preconditionsslides notes video
October 5λ-Calculusnotes video Take-Home Prelim 1
October 7More λ-Calculus and Substitutionslides notes video
October 9de Bruijn and Combinatorsslides notes video Project Charter due
October 12Encodingsslides notes video
October 14Mid-semester break
October 16Encodings and Fixed-Point Combinatorsslides notes video
October 19Definitional Translationslides notes video HW4 due
October 21Continuationsslides notes video
October 23Typesslides notes video
October 26More Typessame slides same notes video HW5 due
October 28Proving Type Soundnessslides notes video
October 30More Proving Type Soundnesssame slides same notes video
November 2Normalizationslides notes video HW6 due
November 4Advanced Typesslides notes video
November 6Polymorphismslides notes video
November 9Type Inferenceslides notes video Take-Home Prelim 2
November 11Recursive Typesslides notes video
November 13Records and Subtypingslides notes video Project Alpha due
November 16Study days
November 18Semi-finals
November 20Semi-finals
November 23Semi-finals
November 25No class (Thanksgiving)
November 27No class (Thanksgiving)
November 30Existential Typesslides notes video
December 2Propositions as Typesslides notes video
December 4Dependent Typesnotes video code Project Beta due
December 7Concurrencyslides video Homework 7 due
December 9Probabilistic Semantics
December 11After 4110 (Guest lecture: TAs)slides video
December 14DSLs and Bidirectional Programmingslides video Homework 8 due
December 16Victory Lapslides video Final Project due