Schedule

DateTopicNotesAssignments
January 24Course Overviewnotes
January 26λ-calculusnotes
January 29More λ-calculussame notes
January 31λ-calculus Encodingsnotes A1 out
February 2Reduction Strategiesnotes
February 5Operational Semanticssame notes
February 7Fixed Pointsnotes
February 9Well-Founded Inductionnotes
February 12Structural Inductionnotes
February 14The IMP Languagenotes A1 due
February 16More IMPsame notes
February 19No class (February Break)
February 21Big-Step Semanticssame notes A2 out
February 23Evaluation Contexts and Translational Semanticsnotes
February 26More Translation and a Functional Languagesame notes proof more
February 28Scopenotes
March 2Snow day!
March 5Statenotes
March 7Continuationsnotes A2 due, Prelim out
March 9No class (Preliminary Exam)
March 12First-Class Continuationsnotes
March 14Axiomatic Semanticsnotes
March 16Hoare Logic & Examplessame notes Prelim due, A3 out
March 19Predicate Transformersnotes
March 21Denotational Semanticsnotes
March 23Typed λ-calculusnotes
March 26NetKAT (guest lecture by Steffen Smolka)
March 28Products, Sums, and Datatypes (guest lecture by Daniel Sainati)notes A3 due
March 30Type Soundnessnotes
April 2No class (Spring Break)
April 4No class (Spring Break)
April 6No class (Spring Break)
April 9Strong Normalizationnotes
April 11Subtypingnotes A4 out
April 13Type Inferencenotes
April 16Polymorphic λ-calculusnotes
April 18More Polymorphismsame notes
April 20Recursive Typesnotes
April 23Objects and Existential Typesnotes
April 25Propositions as Typesnotes more A4 due; A5 out
April 27Linear Typesnotes
April 30Kindsnotes
May 2Dependent Typesnotes A5 proposal due
May 4Guest Lecture by Andrew Myers
May 7Theorem Proversnotes
May 9Program Synthesisnotes code A5 due
May 14Final Exam Available
May 21Final Exam Due