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 30Normalizationslides notes
November 2Advanced TypesHW6 due
November 4Polymorphism
November 6Type Inference
November 9Recursive TypesTake-Home Prelim 2
November 11Records and Subtyping
November 13Existential TypesProject Alpha due
November 16Study days
November 18Semi-finals
November 20Semi-finals
November 23Semi-finals
November 25No class (Thanksgiving)
November 27No class (Thanksgiving)
November 30Propositions as Types
December 2Dependent Types
December 4Probabilistic SemanticsProject Beta due
December 7ConcurrencyHomework 7 due
December 9DSLs
December 11Certified Systems
December 14SynthesisHomework 8 due
December 16Victory LapFinal Project due