August 27 | Course Overview | slides | |

August 30 | Introduction to Semantics | slides notes | |

September 1 | Inductive Definitions | same slides same notes | |

September 3 | Properties and Inductive Proofs | slides notes | |

September 6 | Labor Day | |

September 8 | Inductive Proof | same slides same notes | |

September 10 | Large-Step Semantics | slides notes | |

September 13 | The IMP Language | slides notes | A1 due |

September 15 | IMP Properties | slides notes | |

September 17 | Denotational Semantics | slides notes | |

September 20 | Denotational Semantics Examples | slides notes | A2 due |

September 22 | Axiomatic Semantics | slides notes | |

September 24 | More Axiomatic Semantics | same slides same notes | |

September 27 | Hoare Logic | slides notes | A3 due |

September 29 | Hoare Logic Examples | slides notes | |

October 1 | Weakest Preconditions | slides notes | |

October 4 | λ-Calculus | notes | A4 due |

October 6 | More λ-Calculus and Substitution | slides notes | |

October 8 | Encodings | slides notes | |

October 11 | Fall Break | |

October 13 | Fixed-Point Combinators | slides notes | |

October 15 | de Bruijn and Combinators | slides notes | |

October 18 | Preliminary Exam I | |

October 20 | Definitional Translation | slides notes | |

October 22 | Continuations | slides notes | |

October 25 | Types | slides notes | A5 due |

October 27 | Proving Type Soundness | same slides notes | |

October 29 | More Soundness | same slides same notes | |

November 1 | Normalization | slides notes | A6 due |

November 3 | Advanced Types | slides notes | |

November 5 | Polymorphism | slides notes | |

November 8 | More Polymorphism | same slides same notes | A7 due |

November 10 | Type Inference | slides notes | |

November 12 | Recursive Types | slides notes | |

November 15 | Preliminary Exam II | |

November 17 | Records and Subtyping | slides notes | |

November 19 | Existential Types | slides notes | |

November 22 | Propositions as Types | slides notes | A8 due |

November 24 | No class (Thanksgiving) | |

November 26 | No class (Thanksgiving) | |

November 29 | Linear Types | notes | |

December 1 | Higher-Kinded Types | notes | |

December 3 | Dependent Types | notes | |

December 6 | Synthesis | notes | A9 due |

December 13 | Final Exam, 9:00am, Phillips 101 | |