Schedule

DateTopicNotesAssignments
August 24Course Overviewslides scribbles
August 27Introduction to Semanticsslides notes s1 s2
August 29Inductive Definitionsslides notes s1 s2 A1 out
August 31Properties and Inductive Proofssame slides same notes s1 s2
September 3No class (Labor Day)
September 5Inductive Proof and Large-Step Semanticsslides notes scribbles A1 due; A2 out
September 7The IMP Languageslides notes s1 s2 s3
September 10IMP Propertiesslides notes s1 s2 s3
September 12More IMP Proofssame slides same notes scribbles A2 due; A3 out
September 14Denotational Semanticsslides notes scribbles
September 17Denotational Semantics Examplesslides notes scribbles
September 19Axiomatic Semanticsslides notes s1 s2 A3 due; A4 out
September 21Hoare Logicslides notes s1 s2
September 24Hoare Logic Examplesslides notes s1 s2
September 26Weakest Preconditionsslides notes s1 s2 A4 due
September 28λ-Calculusnotes scribbles
October 1More λ-Calculus and Substitutionslides notes s1 s2
October 3Preliminary Exam I
October 5de Bruijn and Combinatorsslides notes scribbles
October 8No class (Fall Break)
October 10Encodingssame slides same notes scribbles A5 out
October 12Encodings and Fixed-Point Combinatorsslides notes scribbles
October 15Definitional Translationslides notes s1 s2
October 17Continuationssame slides same notes scribbles A5 due; A6 out
October 19Typesnotes s1 s2
October 22More Typessame notes s1 s2
October 24Proving Type Soundnessslides notes scribbles A6 due; A7 out
October 26Normalizationslides notes s1 s2
October 29Advanced Typesslides notes scribbles
October 31Polymorphismslides notes scribbles A7 due; A8 out
November 2Type Inferenceslides notes
November 5Recursive Typesslides notes scribbles
November 7Records and Subtypingslides notes scribbles A8 due
November 9Existential Typesslides notes scribbles
November 12Propositions as Typesslides notes scribbles
November 14Preliminary Exam II
November 16Linear Typesnotes scribbles
November 19Higher-Kinded Typesnotes scribbles
November 21No class (Thanksgiving)
November 23No class (Thanksgiving)
November 26Dependent Typesnotes scribbles
November 28Theorem Proversnotes A9 out
November 30Probabilistic Programmingslides notes code
December 3Victory Lap
December 5No class (semester's over)A9 due
December 12Final Exam at 9am in Hollister B14