August 24 | Course Overview | slides scribbles | |

August 27 | Introduction to Semantics | slides notes s1 s2 | |

August 29 | Inductive Definitions | slides notes s1 s2 | A1 out |

August 31 | Properties and Inductive Proofs | same slides same notes s1 s2 | |

September 3 | No class (Labor Day) | |

September 5 | Inductive Proof and Large-Step Semantics | slides notes scribbles | A1 due; A2 out |

September 7 | The IMP Language | slides notes s1 s2 s3 | |

September 10 | IMP Properties | slides notes s1 s2 s3 | |

September 12 | More IMP Proofs | same slides same notes scribbles | A2 due; A3 out |

September 14 | Denotational Semantics | slides notes scribbles | |

September 17 | Denotational Semantics Examples | slides notes scribbles | |

September 19 | Axiomatic Semantics | slides notes s1 s2 | A3 due; A4 out |

September 21 | Hoare Logic | slides notes s1 s2 | |

September 24 | Hoare Logic Examples | slides notes s1 s2 | |

September 26 | Weakest Preconditions | slides notes s1 s2 | A4 due |

September 28 | λ-Calculus | notes scribbles | |

October 1 | More λ-Calculus and Substitution | slides notes s1 s2 | |

October 3 | Preliminary Exam I | |

October 5 | de Bruijn and Combinators | slides notes scribbles | |

October 8 | No class (Fall Break) | |

October 10 | Encodings | same slides same notes scribbles | A5 out |

October 12 | Encodings and Fixed-Point Combinators | slides notes scribbles | |

October 15 | Definitional Translation | slides notes s1 s2 | |

October 17 | Continuations | same slides same notes scribbles | A5 due; A6 out |

October 19 | Types | notes s1 s2 | |

October 22 | More Types | same notes s1 s2 | |

October 24 | Proving Type Soundness | slides notes scribbles | A6 due; A7 out |

October 26 | Normalization | slides notes s1 s2 | |

October 29 | Advanced Types | slides notes scribbles | |

October 31 | Polymorphism | slides notes scribbles | A7 due; A8 out |

November 2 | Type Inference | slides notes | |

November 5 | Recursive Types | slides notes scribbles | |

November 7 | Records and Subtyping | slides notes scribbles | A8 due |

November 9 | Existential Types | slides notes scribbles | |

November 12 | Propositions as Types | slides notes scribbles | |

November 14 | Preliminary Exam II | |

November 16 | Linear Types | notes scribbles | |

November 19 | Higher-Kinded Types | notes scribbles | |

November 21 | No class (Thanksgiving) | |

November 23 | No class (Thanksgiving) | |

November 26 | Dependent Types | notes scribbles | |

November 28 | Theorem Provers | notes | A9 out |

November 30 | Probabilistic Programming | slides notes code | |

December 3 | Victory Lap | | |

December 5 | No class (semester's over) | A9 due |

December 12 | Final Exam at 9am in Hollister B14 | |