All dates for lectures and unreleased assignments are provisional. Notes from Spring 2009 and Spring 2010 are likely to be close approximations.
| Lecture | Date | Topic/notes | Readings | Assignments, etc. | |
|---|---|---|---|---|---|
| 1 | Jan 21 | Course overview | Pierce Ch. 1–2 | ||
| Operational semantics | |||||
| 2 | Jan 23 | Lambda calculus | Pierce Ch 5.1–2 | ||
| 25 | Recitation: OCaml (S. Basu) | ||||
| 3 | 28 | Lambda calculus encodings, CBV and CBN semantics | Pierce 5.3–4 | ||
| 4 | 30 | Substitution, big-step vs. small-step SOS | Pierce 3.1–2,4-5 | ||
| 5 | Feb 1 | Imperative semantics: IMP | Pierce 3.3,6, Winskel Ch 2 | PS1 out | |
| 6 | 4 | Inductive definitions | Winskel 3.1–3 | ||
| 7 | 6 | Well-founded induction and rule induction | Winskel 4.1–4, Pierce 21.1 | ||
| 8 | 8 | Evaluation contexts, semantics by translation | |||
| 9 | 11 | Strong typing | PS1 due | ||
| Language features | |||||
| 10 | Feb 13 | Naming and scope | PS2 out | ||
| 11 | 15 | Recursive bindings and modules | |||
| 12 | 18 | State and mutable variables, call by reference | |||
| 13 | 20 | Continuation-passing style | |||
| 14 | 22 | Errors and exceptions in CPS | |||
| 15 | 25 | State in CPS and first-class continuations | PS2 due | ||
| 16 | 27 | Compiling with continuations | |||
| Axiomatic semantics | |||||
| 17 | Mar 1 | Hoare logic | Winskel 6 | ||
| 18 | 4 | Predicate transformers | Winskel 7 | PS3 out | |
| Denotational semantics | |||||
| 19 | Mar 6 | Denotational semantics of IMP | Winskel 5 | ||
| 20 | 8 | The Fixed-Point Theorem | Winskel 5 | ||
| 21 | 11 | Domain constructions | Winskel 8 | ||
| 22 | 13 | Recursive functions | Winskel 9 | PS3 due 3/12 | |
| 23 | 15 | Preliminary examination | |||
| Mar 15 | Prelim (in-class) | ||||
| Mar 18 | Spring break | ||||
| Mar 20 | Spring break | ||||
| Mar 22 | Spring break | ||||
| 24 | 25 | Nondeterminism and powerdomains | PS4 out 3/24 | ||
| Types | |||||
| 25 | Mar 27 | Simply typed lambda calculus | Pierce 8.1–2, 9.1–2, 9.5–9.6, 10.1–3, Winskel 11.1–3 | ||
| 26 | 29 | Products, sums, and more | Pierce 11.1–10, Winskel 11.11 | ||
| 27 | Apr 1 | Soundness of the type system | Pierce 8.3, 9.3, Winskel 11.9 | ||
| 28 | 3 | Subtype polymorphism | Pierce 15.1–6 | PS4 due | |
| 29 | 5 | Proof normalization and minimal typing | Pierce 16 | PS5 out | |
| 30 | 8 | Propositions as types | Pierce 9.4, Wadler | ||
| 31 | 10 | Type inference | Pierce 22.1–5 | ||
| 32 | 12 | Parametric polymorphism | Pierce 22.6–7, 23 | ||
| 33 | 15 | Strong normalization and logical relations | Pierce 12 | ||
| 34 | 17 | Recursive types | Pierce 20, Winskel 13 | ||
| More domain theory | |||||
| 35 | Apr 19 | Solving domain equations with D∞ | Winskel 12, Mitchell 7 | PS5 due, PS6 out | |
| 36 | 22 | Abstract interpretation | |||
| Advanced features | |||||
| 37 | Apr 24 | Existential types | Pierce 24, CW86 | ||
| 38 | 26 | Parameterized types and higher-order polymorphism | Pierce 29–30, PJM97, Sec. 3 | ||
| 39 | 29 | Bounded quantification and object encodings | Pierce 18, 26, Comparing Object Encodings | ||
| 40 | May 1 | Object calculus and more OO features | |||
| 41 | 3 | Language-based security | Myers POPL 2013 keynote | PS6 due | |
| May 13 | Final exam, 9:00AM-11:30AM, Bard Hall 140 | ||||