Lecture topics and assignment due dates are subject to change.

DATE | EVENT | TOPIC | READINGS | LINKS |
---|---|---|---|---|

Operational Semantics and Proof Techniques | ||||

1/25 | Lecture 1 | Course Introduction | [Notes] | |

1/25 | Assignment 1 issued | [A1] | ||

1/27 | Lecture 2 | The λ-Calculus | [Notes][Handout] | |

1/28 | OCaml demo, 7:30–9pm, Upson B7 Lab | [fv.ml] | ||

1/29 | Lecture 3 | λ-Calculus Encodings | [Notes] | |

2/1 | Lecture 4 | Reduction Strategies and Equivalence | [Notes] | |

2/3 | Lecture 5 | Recursion and Fixpoint Combinators | [Notes] | |

2/5 | Lecture 6 | Structural Operational Semantics and IMP | [Notes] | |

2/8 | Lecture 7 | Well-Founded Induction | [Notes] | |

2/10 | Assignment 1 due, Assignment 2 issued | [A1] [A2] | ||

2/10 | Lecture 8 | Inductive Definitions and Least Fixpoints | [Notes][Handout] | |

2/12 | Lecture 9 | Evaluation Contexts | [Notes] | |

Language Features | ||||

2/15 | Lecture 10 | Semantics via Translation | [Notes] | |

2/17 | Lecture 11 | A Functional Language | [Notes] | |

2/19 | Lecture 12 | Static vs Dynamic Scope | [Notes] | |

2/22 | Lecture 13 | Modules and State | [Notes][Handout] | |

2/24 | Lecture 14 | Continuations | [Notes] | |

2/26 | Assignment 2 due, Assignment 3 issued | [A2] [A3] | ||

2/26 | Lecture 15 | Continuations and Exceptions | [Notes][Handout] | |

Axiomatic Semantics | ||||

3/1 | Lecture 16 | Predicate Transformers | [Notes] | |

3/3 | Lecture 17 | Hoare Logic | [Notes] | |

3/5 | Lecture 18 | Dynamic Logic and Kleene Algebra | [Notes] | |

3/8 | Lecture 19 | Constructions in Dynamic Logic and Kleene Algebra | [Notes] | |

Denotational Semantics | ||||

3/10 | Lecture 20 | Denotational Semantics of IMP | [Notes] | |

3/12 | Lecture 21 | Denotational Semantics of IMP, cont. | [Notes] | |

3/15 | Assignment 3 due | [A3] | ||

3/12–3/21 | Preliminary Exam | |||

3/15 | Lecture 22 | Domain Constructions | [Notes] | |

3/17 | Lecture 23 | Denotational Semantics of REC | [Notes] | |

3/19 | Lecture 24 | Scott's D_{∞} Construction |
[Notes][Handout] | |

3/20–3/28 | Spring Break | |||

3/29 | Assignment 4 issued | [A4] | ||

Types | ||||

3/29 | Lecture 25 | Typed λ-Calculus | [Notes] | |

3/31 | Lecture 26 | Soundness of the Typing Rules | [Notes] | |

4/2 | Lecture 27 | Products, Sums, and Other Datatypes | [Notes] | |

4/5 | Lecture 28 | Strong Normalization | [Notes] | |

4/7 | Lecture 29 | Type Inference and Unification | [Notes] | |

4/9 | Lecture 30 | The Polymorphic λ-Calculus | [Notes] | |

4/12 | Lecture 31 | Propositions as Types | [Notes] | |

4/14 | Lecture 32 | Propositions as Types II | [Notes][NatDed] | |

4/16 | Assignment 4 due, Assignment 5 issued | [A4] [A5] | ||

4/16 | Lecture 33 | Subtype Polymorphism | [Notes] | |

4/19 | Lecture 34 | Recursive Types | [Notes] | |

4/21 | Lecture 35 | Testing Equirecursive Equality | [Notes] | |

4/23 | Lecture 36 | Coinductive Subtyping of Recursive Types | [Notes] | |

4/26 | Lecture 37 | Type Inference for Partial Types | [Notes] | |

4/28 | Lecture 38 | Abstract Interpretation | [Notes] | |

Topics | ||||

4/30 | Lecture 39 | Abstract Interpretation (cont.) | [Notes] | |

5/3 | Assignment 5 due | [A5] | ||

5/3 | Lecture 40 | Existential Types | [Notes] | |

5/5 | Lecture 41 | Object-Oriented Languages | [Notes] | |

5/7 | Lecture 42 | Monads | [Notes][Wadler][Moggi] | |

5/7–5/17 | Final Exam |