January 24 | Course Overview | notes | |

January 26 | λ-calculus | notes | |

January 28 | More λ-calculus | same notes more | |

January 31 | λ-calculus Encodings | notes | A1 out |

February 2 | Reduction Strategies | notes | |

February 4 | No lecture (snow day) | | |

February 7 | Operational Semantics | same notes | |

February 9 | Fixed Points | notes | |

February 11 | Well-Founded Induction | notes | |

February 14 | Structural Induction | notes | |

February 16 | The IMP Language | notes | |

February 18 | More IMP | same notes | A2 out |

February 21 | Big-Step Semantics | same notes | |

February 23 | Big-Step and Evaluation Contexts | notes | |

February 25 | no lecture | | |

February 28 | no lecture (February break) | | |

March 2 | More Translation | same notes proof | |

March 4 | Functional Language | same notes | |

March 7 | Functional Language (recursion) | same notes | |

March 9 | Scope | notes | |

March 11 | Revision for Prelim (exercises) | | |

March 14 | State | notes | |

March 16 | Strong Typing and Continuations | notes more | Prelim out |

March 18 | More Continuations and Exceptions | same notes more | |

March 21 | Axiomatic Semantics & Hoare Logic | notes | |

March 23 | Weakest Preconditions | notes | Prelim due |

March 25 | Dynamic Logic and Kleene Algebra | notes | |

March 28 | Constructions in Dynamic Logic and Kleene Algebra | same notes | |

March 30 | Typed λ-calculus | notes | |

April 1 | Products, Sums, and Datatypes | notes | |

April 4 | Spring Break | | |

April 6 | Spring Break | | |

April 8 | Spring Break | | |

April 11 | Denotational Semantics | notes | |

April 13 | Partial Orders & Continuity | notes | |

April 15 | Strong Normalization | notes | |

April 18 | Type Inference | notes | |

April 20 | Subtyping | notes | |

April 22 | Polymorphic λ-calculus | notes | |