August 27Course Overviewslides
August 30Introduction to Semanticsslides notes
September 1Inductive Definitionssame slides same notes
September 3Properties and Inductive Proofsslides notes
September 6Labor Day
September 8Inductive Proofsame slides same notes
September 10Large-Step Semanticsslides notes
September 13The IMP Languageslides notes A1 due
September 15IMP Propertiesslides notes
September 17Denotational Semanticsslides notes
September 20Denotational Semantics Examplesslides notes A2 due
September 22Axiomatic Semanticsslides notes
September 24More Axiomatic Semanticssame slides same notes
September 27Hoare Logicslides notes A3 due
September 29Hoare Logic Examplesslides notes
October 1Weakest Preconditionsslides notes
October 4λ-Calculusnotes A4 due
October 6More λ-Calculus and Substitutionslides notes
October 8Encodingsslides notes
October 11Fall Break
October 13Fixed-Point Combinatorsslides notes
October 15de Bruijn and Combinatorsslides notes
October 18Preliminary Exam I
October 20Definitional Translationslides notes
October 22Continuationsslides notes
October 25Typesslides notes A5 due
October 27Proving Type Soundnesssame slides notes
October 29More Soundnesssame slides same notes
November 1Normalizationslides notes A6 due
November 3Advanced Typesslides notes
November 5Polymorphismslides notes
November 8More Polymorphismsame slides same notes A7 due
November 10Type Inferenceslides notes
November 12Recursive Typesslides notes
November 15Preliminary Exam II
November 17Records and Subtypingslides notes
November 19Existential Typesslides notes
November 22Propositions as Typesslides notes A8 due
November 24No class (Thanksgiving)
November 26No class (Thanksgiving)
November 29Linear Typesnotes
December 1Higher-Kinded Typesnotes
December 3Dependent Typesnotes
December 6Synthesisnotes A9 due
December 13Final Exam, 9:00am, Phillips 101