Schedule

DateTopicNotesAssignments
January 24Course Overviewnotes
January 26λ-calculusnotes
January 28More λ-calculussame notes more
January 31λ-calculus Encodingsnotes A1 out
February 2Reduction Strategiesnotes
February 4No lecture (snow day)
February 7Operational Semanticssame notes
February 9Fixed Pointsnotes
February 11Well-Founded Inductionnotes
February 14Structural Inductionnotes
February 16The IMP Languagenotes
February 18More IMPsame notes A2 out
February 21Big-Step Semanticssame notes
February 23Big-Step and Evaluation Contextsnotes
February 25no lecture
February 28no lecture (February break)
March 2More Translationsame notes proof
March 4Functional Languagesame notes
March 7Functional Language (recursion)same notes
March 9Scopenotes
March 11Revision for Prelim (exercises)
March 14Statenotes
March 16Strong Typing and Continuationsnotes more Prelim out
March 18More Continuations and Exceptionssame notes more
March 21Axiomatic Semantics & Hoare Logicnotes
March 23Weakest Preconditionsnotes Prelim due
March 25Dynamic Logic and Kleene Algebranotes
March 28Constructions in Dynamic Logic and Kleene Algebrasame notes
March 30Typed λ-calculusnotes
April 1Products, Sums, and Datatypesnotes
April 4Spring Break
April 6Spring Break
April 8Spring Break
April 11Denotational Semanticsnotes
April 13Partial Orders & Continuitynotes
April 15Strong Normalizationnotes
April 18Type Inferencenotes
April 20Subtypingnotes
April 22Polymorphic λ-calculusnotes