Schedule

DateTopicNotesAssignments
August 25Course Overviewslides Introductory Survey due 8/28
August 27Semanticsslides notes
August 29Inductionslides notes
September 1Labor Day
September 3Lab: Semanticslab
September 5Lab: Inductionlab A1 due 9/4
September 8IMP (Guest: Kozen)slides notes
September 10IMP Properties (Guest: Kozen)slides notes
September 12Lab: IMPlab A2 due 9/11
September 15Denotational Semanticsslides notes
September 17Program Equivalenceslides notes
September 19Lab: Denotational Semanticslab A3 due 9/18
September 22Axiomatic Semanticsslides notes
September 24Hoare Logicslides notes
September 26Lab: Axiomatic Semanticslab handout A4 due 9/25
September 29Predicate Transformers (Guest: Moeller)slides notes
October 1Separation Logicslides notes
October 3Lab: Separation Logiclab A5 due 10/2
October 6Lambda Calculusslides notes
October 8More Lambda Calculusslides notes
October 10Prelim I
October 13Fall Break
October 15Definitional Translation (Guest: Myers)slides notes
October 17Continuations (Guest: Myers)slides notes
October 20Fixed-point Combinatorsslides notes
October 22de Bruijn Notation and Combinatorsslides notes
October 24Lab: Lambda-Calculuslab A6 due 10/23
October 27Type Systemsslides notes
October 29Advanced Typesslides notes
October 31Lab: Type Systemslab A7 due 10/30
November 3Polymorphismslides notes
November 5Making OCaml Safe for Performance Engineering (Guest: Minsky)
November 7Lab: Polymorphismlab A8 due 11/8
November 10Prelim II
November 12Dependent Types and Type Theory (Guest: Barbone)
November 14Lab:Type Theory (Guest: Barbone)
November 17Normalization
November 19Logical Relations
November 21Lab:Logical RelationsA9 due 11/20
November 24Logic Programming
November 26Thanksgiving Break
November 28Thanksgiving Break
December 1Lenses
December 3Program Synthesis
December 5Lab: Domain-Specific LanguagesA10 due 12/4
December 8Victory Lap
December 16Final Exam (7:00-9:30pm)