January 23 | Course Overview | notes | |
January 25 | λ-calculus | notes | |
January 28 | More λ-calculus | same notes | |
January 30 | λ-calculus Encodings | notes | A1 out |
February 1 | Reduction Strategies | notes | |
February 4 | Operational Semantics | same notes | |
February 6 | Fixed Points | notes | |
February 8 | Well-Founded Induction | notes | |
February 11 | Structural Induction | notes | |
February 13 | The IMP Language | notes | A1 due, A2 out |
February 15 | More IMP | same notes | |
February 18 | Big-Step Semantics | same notes | |
February 20 | Evaluation Contexts and Translational Semantics | notes | |
February 22 | More Translation and a Functional Language | same notes proof more | |
February 25 | No class (February Break) | |
February 27 | Scope | notes | |
March 1 | State | notes | |
March 4 | Continuations | notes | |
March 6 | More Continuations and Exceptions | same notes | A2 due, Prelim out |
March 8 | No class (Preliminary Exam) | |
March 11 | First-Class Continuations | notes code | |
March 13 | Axiomatic Semantics & Hoare Logic | notes | Prelim due, A3 out |
March 15 | Weakest Preconditions | notes | |
March 18 | Denotational Semantics | notes | |
March 20 | Partial Orders & Continuity | notes | |
March 22 | More CPOs | same notes | |
March 25 | Typed λ-calculus | notes | |
March 27 | Products, Sums, and Datatypes | notes | A3 due |
March 29 | Type Soundness | notes | |
April 1 | No class (Spring Break) | |
April 3 | No class (Spring Break) | |
April 5 | No class (Spring Break) | |
April 8 | Strong Normalization | notes | |
April 10 | Subtyping | notes | A4 out |
April 12 | Type Inference | notes | |
April 15 | Polymorphic λ-calculus | notes | |
April 17 | More Polymorphism | same notes | |
April 19 | Recursive Types | notes | |
April 22 | Objects and Existential Types | notes | |
April 24 | Propositions as Types | notes more | A4 due; A5 out |
April 26 | Linear Types | notes | |
April 29 | Kinds | notes | |
May 1 | Dependent Types | notes | A5 proposal due |
May 3 | Theorem Provers (guest lecture by Andrew Hirsch) | notes code | |
May 6 | Program Synthesis | notes code | |
May 9 | No class (semester's over) | A5 due |
May 8 | Final Exam Available | |
May 15 | Final Exam Due | |