|
|||||
| # | Date | Topic | Readings* | Lecture notes ( =slides) |
Homework |
|---|---|---|---|---|---|
| Operational semantics and proof techniques | |||||
| 1 | Jan. 19 | Course introduction | P1,2 | [ PDF ] | |
| Rec 1 | 26 | OCaml tutorial (Jed Liu) | Introduction to Objective Caml |
| |
| 2 | 28 | Lambda calculus encodings and recursion | P5.1–5.2 | [ 2007 PDF | LaTeX ] [ 2005 PDF ] | |
| 3 | 30 | Normal forms, confluence, CBV vs. CBN | P5.3–5.4 | [ PDF | LaTeX ] | |
| 4 | Feb. 2 | Substitution, big-step vs. small-step SOS | P3.1,3.2,3.4,3.5 | [ PDF | LaTeX ] | |
| 5 | 4 | IMP | P3.3,3.6,W2 | [ PDF | LaTeX ] | handout: PS1 |
| 6 | 6 | Inductive definitions | W3.1–3.3 | [ PDF | LaTeX ] | |
| 7 | 9 | Well-founded induction and rule induction | W4.1–4.4, P21.1 | [ PDF | LaTeX ] | |
| 8 | 11 | Evaluation contexts, semantics by translation | [ PDF | LaTeX ] | due: PS1 |
|
| Language features and translations | |||||
| 9 | 13 | uML and strong typing | [ PDF | LaTeX ] | ||
| 10 | 16 | Naming and scope | [ PDF | LaTeX ] | handout: PS2 | |
| 11 | 18 | Recursive bindings and modules | [ PDF | LaTeX ] | ||
| 12 | 20 | State and mutable variables | [ PDF | LaTeX ] | ||
| 13 | 23 | Call by reference, continuation-passing style, CPS conversion | [ PDF | LaTeX ] | ||
| 14 | 25 | Nonlocal control: errors and exceptions | [ PDF | LaTeX ] | due: PS2 (Feb. 26) | |
| 15 | 27 | First-class continuations and threads | [ PDF | LaTeX ] | handout: PS3 (Feb. 26) | |
| 16 | Mar. 2 | Compiling with continuations | [ PDF | LaTeX ] | ||
| Axiomatic semantics | |||||
| 17 | 4 | Hoare logic | 10 Years of Hoare's Logic, §1,2 (Apt), (W6) | (No notes; read Winskel.) | |
| 18 | 6 | Weakest preconditions | Predicate Transformers (Dijkstra) (W7) | ||
| 19 | 9 | Verification conditions and applications | [ PDF | LaTeX ] | ||
| Denotational (fixed-point) semantics | |||||
| 20 | 11 | Denotational semantics of IMP | W5.1–5.2 | [ PDF | LaTeX ] | due: PS3 (Mar. 12) |
| 21 | 13 | The Fixed-Point Theorem | W5.3–5.4 | [ PDF | LaTeX ] | |
| Mar. 16–20 |
No class: spring break |
||||
| 22 | 23 | Domain constructions | W8.1–4 | [ PDF | LaTeX ] | |
| 23 | 25 | Metalanguage for denotational semantics | W9.1–3,5–6 | [ PDF | LaTeX ] | |
| March 26 | Prelim, 7:30–9:30PM, 110 Hollister Hall. Covers lectures 1–22. | See CMS for sample prelim | |||
| 27 | No class (post-exam) | ||||
| Static semantics (type systems) | |||||
| 24 | 30 | Simply-typed lambda calculus | P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 | [ PDF | LaTeX ] | |
| 25 | Apr. 1 | Products, sums, and more | P11.1–10, (W11.11) | [ PDF | LaTeX ] | |
| 26 | 3 | Soundness of the type system | P8.3, P9.3, (W11.9) | [ PDF | LaTeX ] | |
| 27 | 6 | Subtype polymorphism | P15.1–6 (Gunter 9) | [ PDF | LaTeX ] | |
| 28 | 8 | Proof normalization and minimal typing | P16 | [ PDF | LaTeX ] | |
| 29 | 10 | Type inference | P22.1–5 | [ PDF | LaTeX ] | |
| 30 | 13 | Parametric polymorphism | P22.6–7, P23 | [ PDF | LaTeX ] | |
| 31 | 15 | Strong normalization and logical relations | P12 | [ PDF | LaTeX ] | |
| 32 | 17 | Propositions as types | Wadler, P9.4 | [ PDF | LaTeX ] | due: PS4 |
| 33 | 20 | Recursive types | P20, W13 (Gunter 5, 10) | [ PDF | LaTeX ] | |
| 34 | 22 | Solving domain equations | W12, M7, Gunter 5, 9 | [ PDF | LaTeX ] | |
| 35 | 24 | Existential types | P24–24.2 CW86 (Mitchell 9.4–9.5) | [ PDF | LaTeX ] | |
| 36 | 27 | Parameterized types and higher-order polymorphism | P29–30 | [ PDF (2005) | LaTeX ] | |
| 37 | 29 | Bounded quantification and object encodings | P18, P26, (AC 1-5) Bruce et al. (Local copy in CMS) |
|
|
| 38 | May 1 | More object-oriented features | (AC 6–8, NCM04) |
|
due: PS5 |
| May 11 | Final Exam, 9:00–11:30am, 206 Hollister Hall | ||||
P = Pierce, W = Winskel, M = Mitchell, AC = Abadi & Cardelli
CS 611 Spring 2009