Schedule

DateTopicNotesAssignments
January 22Course Overviewslides
January 24Introduction to Semanticsslides notes
January 26Inductive Definitionssame slides same notes
January 29Small-Step Semanticssame slides same notes
January 31Properties and Inductive Proofsslides notes
February 2Inductive Proof Practicesame slides same notes
February 5Large-Step Semanticsslides notes
February 7The IMP Languageslides notes
February 9IMP Propertiesslides notes A1 due 2/8
February 12Denotational Semanticsslides notes
February 14More Denotationssame slides same notes
February 16Denotational Semantics Proofsslides notes A2 due 2/15
February 19Axiomatic Semanticsslides notes
February 21Hoare Logicslides notes
February 23Hoare Logic Examplesslides notes A3 due 2/22
February 26February Break
February 28Weakest Preconditionsslides notes
March 1λ-Calculusnotes
March 4More λ-Calculus and Substitutionslides notes A4 due 3/3
March 6Encodingsslides notes
March 8Preliminary Exam I
March 11Fixed-Point Combinatorsslides notes
March 13de Bruijn and Combinatorsslides notes
March 15Definitional Translationslides notes A5 due 3/14
March 18Continuationsslides notes
March 20Typesslides notes
March 22Proving Type Soundnesssame slides notes A6 due 3/21
March 25More Soundnesssame slides same notes
March 27Normalizationslides notes
March 29Advanced Typesslides notes A7 due 3/28
April 1Spring Break
April 3Spring Break
April 5Spring Break
April 8Polymorphismslides notes
April 10More Polymorphismsame slides same notes
April 12Type Inferenceslides notes
April 15Recursive Typesslides notes A8 due 4/14
April 17Records and Subtypingslides notes
April 19Preliminary Exam II
April 22Existential Typesslides notes
April 24Propositions as Typesslides notes
April 26Linear Typesnotes A9 due 4/25
April 29Packet Scheduling (with guest lecturer Anshuman Mohan)speaker
May 1Synthesis (with guest lecturer Vivian Ding)speaker
May 3Higher-Kinded Typesnotes A10 due 5/2
May 6Dependent Typesnotes
May 13Final Exam, 9am in Hollister B14