|
||||||
| # | Date | Topic | Readings* | Lecture notes ( =slides) |
Homework | |
|---|---|---|---|---|---|---|
| Operational semantics and proof techniques | ||||||
| 1 | Aug. 24 | Course introduction | P1,2 | [ PDF ] | handout: PS1 (Part 3) | |
| 2 | 27 | Lambda calculus | P5.1–5.2 | [ PDF | LaTeX ] | ||
| 3 | 29 | Lambda calculus encodings and recursion | P5.3–5.4 | [ PDF | LaTeX ] | ||
| 4 | 31 | Normal forms | P3.1,3.2,3.4,3.5 | [ PDF | LaTeX ] | ||
| 5 | Sept. 3 | Big-step vs. small-step SOS | P3.3,3.6,W2 | [ PDF | LaTeX ] | ||
| 6 | 5 |
Well-founded induction and function definitions |
W3.1–3.3 | [ PDF | LaTeX ] | due: PS1 handout: PS2 |
|
| 7 | 7 | Inductive definitions and rule induction | W4.1–4.4, P21.1 | [ PDF | LaTeX ] | ||
| 8 | 10 | Evaluation contexts | [ PDF | LaTeX ] | |||
| Language features and translations | ||||||
| 9 | 12 | Semantics via translation | [ PDF | LaTeX ] | |||
| 10 | 14 | uML, strong typing, scope | [ PDF | LaTeX ] | due: PS2a handout: PS3 |
||
| 11 | 17 | Naming (Lecturer: Steve Chong) | [ PDF | LaTeX ] | |||
| 12 | 19 | Closures (Lecturer: Dexter Kozen) | [ PDF | LaTeX ] | |||
| 13 | 21 | Modules and state | [ PDF | LaTeX ] | due: PS2b | ||
| 14 | 24 | State and mutable variables | [ PDF | LaTeX ] | |||
| 15 | 26 | Continuation-passing style and CPS conversion | [ PDF | LaTeX ] | |||
| 16 | 28 | Nonlocal control: errors and exceptions | [ PDF | LaTeX ] | due: PS3 | ||
| 17 | Oct. 1 | First-class continuations, compiling with continuations | [ PDF | LaTeX ] | handout: PS4 | ||
| Axiomatic semantics | ||||||
| 18 | 3 | Hoare logic | 10 Years of Hoare's Logic, §1,2 (Apt), (W6) | (No notes; read Winskel.) | ||
| 19 | 5 | Weakest preconditions | Predicate Transformers (Dijkstra) (W7) | |||
| 8 |
No class: fall break |
|||||
| Denotational (fixed-point) semantics | ||||||
| 20 | 10 | Denotational semantics of IMP | W5.1–5.2 | [ PDF | LaTeX ] | ||
| 21 | 12 | The Fixed-Point Theorem | W5.3–5.4 | [ PDF | LaTeX ] | ||
| 22 | 15 | Domain constructions (Lecturer: Dexter Kozen) | W8.1–4 | [ PDF | LaTeX ] | ||
| 23 | 17 | Metalanguage for denotational semantics (Lecturer: Dexter Kozen) | ||||
| 24 | 19 | Denotational semantics of functions | W9.1–3,5–6 | [ PDF | LaTeX ] | due: PS4 | |
| 25 | 22 | Solving domain equations | W12, M7, Gunter 5, 9 | [ PDF | LaTeX ] | ||
| Oct. 23 | Prelim, 7:30–9:30PM, Upson 109. Covers lectures 1–24 (incl. REC semantics) | See CMS for sample prelim | ||||
| Static semantics (type systems) | ||||||
| 24 | No class (post-exam) | |||||
| 26 | 26 | Simply-typed lambda calculus | P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 | [ PDF | LaTeX ] | ||
| 27 | 29 | Products, sums, and more | P11.1–10, (W11.11) | [ PDF | LaTeX ] | handout: PS5 (q3) | |
| 28 | 31 | Soundness of the type system | P8.3, P9.3, (W11.9) | [ PDF | LaTeX ] | ||
| 29 | Nov. 2 | Logical relations and strong normalization | P12, (W11.4–8) | [ PDF | LaTeX ] | ||
| 30 | 5 | Recursive types | P20, W13 (Gunter 5, 10) | [ PDF | LaTeX ] | ||
| 31 | 7 | Subtype polymorphism (Lecturer: Radu Rugina) |
P15.1–6 (Gunter 9) | [ PDF | LaTeX ] | ||
| 32 | 9 | Type inference | P22.1–5 | [ PDF | LaTeX ] | ||
| 33 | 12 | Parametric polymorphism | P22.6–7, P23 | [ PDF | LaTeX ] | ||
| 34 | 14 | Recitation | due: PS5 | |||
| 35 | 16 | Propositions as types | Wadler | [ PDF | LaTeX ] | handout: PS6 | |
| 36 | 19 | Existential types | P24–24.2 CW86 (Mitchell 9.4–9.5) | [ PDF | LaTeX ] | ||
| 37 | 21 | Parameterized types and higher-order polymorphism | P29–30 | [ PDF (2005) | LaTeX ] | ||
| 23 | No class: Thanksgiving break | |||||
| 38 | 26 | Object-oriented languages | P18, (AC 1-4) |
|
||
| 39 | 28 | Object calculi and encodings | (AC 5–8) |
|
||
| 40 | 30 | Bounded quantification and directions in PL research | P26, (MLB97, M99, ZCMZ03, NCM04, LM06) |
|
due: PS6 | |
| Dec. 12 | Final Exam, 7:00–9:30pm, Hollister 362 | |||||
P = Pierce, W = Winskel, M = Mitchell, AC = Abadi & Cardelli
CS 611 Fall 2007