January 23Course Overviewnotes
January 25λ-calculusnotes
January 28More λ-calculussame notes
January 30λ-calculus Encodingsnotes A1 out
February 1Reduction Strategiesnotes
February 4Operational Semanticssame notes
February 6Fixed Pointsnotes
February 8Well-Founded Inductionnotes
February 11Structural Inductionnotes
February 13The IMP Languagenotes A1 due, A2 out
February 15More IMPsame notes
February 18Big-Step Semanticssame notes
February 20Evaluation Contexts and Translational Semanticsnotes
February 22More Translation and a Functional Languagesame notes proof more
February 25No class (February Break)
February 27Scopenotes
March 1Statenotes
March 4Continuationsnotes
March 6More Continuations and Exceptionssame notes A2 due, Prelim out
March 8No class (Preliminary Exam)
March 11First-Class Continuationsnotes code
March 13Axiomatic Semantics & Hoare Logicnotes Prelim due, A3 out
March 15Weakest Preconditionsnotes
March 18Denotational Semanticsnotes
March 20Partial Orders & Continuitynotes
March 22More CPOssame notes
March 25Typed λ-calculusnotes
March 27Products, Sums, and Datatypesnotes A3 due
March 29Type Soundnessnotes
April 1No class (Spring Break)
April 3No class (Spring Break)
April 5No class (Spring Break)
April 8Strong Normalizationnotes
April 10Subtypingnotes A4 out
April 12Type Inferencenotes
April 15Polymorphic λ-calculusnotes
April 17More Polymorphismsame notes
April 19Recursive Typesnotes
April 22Objects and Existential Typesnotes
April 24Propositions as Typesnotes more A4 due; A5 out
April 26Linear Typesnotes
April 29Kindsnotes
May 1Dependent Typesnotes A5 proposal due
May 3Theorem Provers (guest lecture by Andrew Hirsch)notes code
May 6Program Synthesisnotes code
May 9No class (semester's over)A5 due
May 8Final Exam Available
May 15Final Exam Due