Schedule
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 | |||