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 |