January 22 | Course Overview | slides | |

January 24 | Introduction to Semantics | slides notes | |

January 26 | Inductive Definitions | same slides same notes | |

January 29 | Small-Step Semantics | same slides same notes | |

January 31 | Properties and Inductive Proofs | slides notes | |

February 2 | Inductive Proof Practice | same slides same notes | |

February 5 | Large-Step Semantics | slides notes | |

February 7 | The IMP Language | slides notes | |

February 9 | IMP Properties | slides notes | A1 due 2/8 |

February 12 | Denotational Semantics | slides notes | |

February 14 | More Denotations | same slides same notes | |

February 16 | Denotational Semantics Proofs | slides notes | A2 due 2/15 |

February 19 | Axiomatic Semantics | slides notes | |

February 21 | Hoare Logic | slides notes | |

February 23 | Hoare Logic Examples | slides notes | A3 due 2/22 |

February 26 | February Break | |

February 28 | Weakest Preconditions | slides notes | |

March 1 | λ-Calculus | notes | |

March 4 | More λ-Calculus and Substitution | slides notes | A4 due 3/3 |

March 6 | Encodings | slides notes | |

March 8 | Preliminary Exam I | |

March 11 | Fixed-Point Combinators | slides notes | |

March 13 | de Bruijn and Combinators | slides notes | |

March 15 | Definitional Translation | slides notes | A5 due 3/14 |

March 18 | Continuations | slides notes | |

March 20 | Types | slides notes | |

March 22 | Proving Type Soundness | same slides notes | A6 due 3/21 |

March 25 | More Soundness | same slides same notes | |

March 27 | Normalization | slides notes | |

March 29 | Advanced Types | slides notes | A7 due 3/28 |

April 1 | Spring Break | |

April 3 | Spring Break | |

April 5 | Spring Break | |

April 8 | Polymorphism | slides notes | |

April 10 | More Polymorphism | same slides same notes | |

April 12 | Type Inference | slides notes | |

April 15 | Recursive Types | slides notes | A8 due 4/14 |

April 17 | Records and Subtyping | slides notes | |

April 19 | Preliminary Exam II | |

April 22 | Existential Types | slides notes | |

April 24 | Propositions as Types | slides notes | |

April 26 | Linear Types | notes | A9 due 4/25 |

April 29 | Synthesis | notes | |

May 1 | Special Topic | | |

May 3 | Higher-Kinded Types | notes | A10 due 5/2 |

May 6 | Dependent Types | notes | |

May 13 | Final Exam, 9am | |