January 25Course Overviewslides notes
January 27λ-calculusnotes
January 30More λ-calculussame notes
February 1λ-calculus Encodingsnotes A1 out
February 3Reduction Strategies, Operational Semanticsnotes
February 6Fixed Pointsnotes
February 8Well-Founded Induction and Structural Inductionnotes
February 10More Structural Inductionnotes
February 13The IMP Languagenotes
February 15More IMP and Big-Step Operational Semanticssame notes A1 due
February 17Big-Step Semantics and Evaluation Contextsnotes
February 20No class (February Break)
February 22Semantics via Translation and a Functional Languagesame notes proof more A2 out
February 24Scopenotes
February 27Statenotes
March 1Continuationsnotes
March 3Proof Writing, with special guest Andrew Hirsch
March 6First-Class Continuations and Axiomatic Semanticsnotes more
March 8Axiomatic Semantics and Hoare Logicsame notes A2 due, A3 out
March 10Predicate Transformersnotes
March 13Denotational Semanticsnotes
March 15Snow day!
March 17Typed λ-calculusnotes
March 20Type Soundnessnotes
March 22Type Soundness, continuedsame notes A3 due
March 24Products, Sums, and Datatypesnotes
March 27Strong Normalizationnotes Prelim out
March 29Strong Normalization, continuedsame notes
March 31Preliminary Exam Due
April 3No class (Spring Break)
April 5No class (Spring Break)
April 7No class (Spring Break)
April 10Type Inferencenotes
April 12Polymorphic λ-calculusnotes A4 out
April 14More Polymorphismsame notes
April 17Subtypingnotes
April 19Recursive Typesnotes
April 21Objects and Existential Typesnotes
April 24Propositions as Typesnotes
April 26More Propositions as Typesnotes A4 due; A5 out
April 28Linear Typesnotes
May 1Kindsnotes
May 3Dependent Typesnotes A5 proposal due
May 5Theorem Proversnotes
May 8Gradual typing, with special guest Fabian Muehlboecknotes
May 10No classA5 due
Tuesday, May 23Final Exam, 9–11:30am, Gates G01