January 25 | Course Overview | slides notes | |

January 27 | λ-calculus | notes | |

January 30 | More λ-calculus | same notes | |

February 1 | λ-calculus Encodings | notes | A1 out |

February 3 | Reduction Strategies, Operational Semantics | notes | |

February 6 | Fixed Points | notes | |

February 8 | Well-Founded Induction and Structural Induction | notes | |

February 10 | More Structural Induction | notes | |

February 13 | The IMP Language | notes | |

February 15 | More IMP and Big-Step Operational Semantics | same notes | A1 due |

February 17 | Big-Step Semantics and Evaluation Contexts | notes | |

February 20 | No class (February Break) |

February 22 | Semantics via Translation and a Functional Language | same notes proof more | A2 out |

February 24 | Scope | notes | |

February 27 | State | notes | |

March 1 | Continuations | notes | |

March 3 | Proof Writing, with special guest Andrew Hirsch | | |

March 6 | First-Class Continuations and Axiomatic Semantics | notes more | |

March 8 | Axiomatic Semantics and Hoare Logic | same notes | A2 due, A3 out |

March 10 | Predicate Transformers | notes | |

March 13 | Denotational Semantics | notes | |

March 15 | Snow day! |

March 17 | Typed λ-calculus | notes | |

March 20 | Type Soundness | notes | |

March 22 | Type Soundness, continued | same notes | A3 due |

March 24 | Products, Sums, and Datatypes | notes | |

March 27 | Strong Normalization | notes | Prelim out |

March 29 | Strong Normalization, continued | same notes | |

March 31 | Preliminary Exam Due |

April 3 | No class (Spring Break) |

April 5 | No class (Spring Break) |

April 7 | No class (Spring Break) |

April 10 | Type Inference | notes | |

April 12 | Polymorphic λ-calculus | notes | A4 out |

April 14 | More Polymorphism | same notes | |

April 17 | Subtyping | notes | |

April 19 | Recursive Types | notes | |

April 21 | Objects and Existential Types | notes | |

April 24 | Propositions as Types | notes | |

April 26 | More Propositions as Types | notes | A4 due; A5 out |

April 28 | Linear Types | notes | |

May 1 | Kinds | notes | |

May 3 | Dependent Types | notes | A5 proposal due |

May 5 | Theorem Provers | notes | |

May 8 | Gradual typing, with special guest Fabian Muehlboeck | notes | |

May 10 | No class | | A5 due |

Tuesday, May 23 | Final Exam, 9–11:30am, Gates G01 |