CS611 Fall 2006 Schedule
This schedule is subject to change and is only intended as a rough guide.
Well-founded induction and function definitions
|
|||||
| # | Date | Topic | Readings | Notes | Homework |
|---|---|---|---|---|---|
| Operational Semantics and Proof Techniques | |||||
| 1 | Aug 25 | Course introduction | P1,2 | [ PDF | LaTeX ] | handout: PS1 |
| 28 | SML tutorial | Executable SML tutorial, SML cheatsheet [PDF] | |||
| 2 | 30 | Lambda calculus | P5.1–5.2 | [ PDF | LaTeX ] | |
| 3 | Sep 1 | Normal forms | P3.1,3.2,3.4,3.5 | [ PDF | LaTeX ] | |
| 4 | No class: Labor Day | ||||
| 4 | 6 | Lambda calculus encodings and recursion | P5.3–5.4 | [ PDF | LaTeX ] | due: PS1 |
| 5 | 8 | Big-step vs. small-step SOS | P3.3,3.6,W2 | [ PDF | LaTeX ] | |
| 6 | 11 |
Well-founded induction and function definitions |
W3.1–3.3 | [ PDF | LaTeX ] | handout: PS2 |
| 7 | 13 | Inductive definitions and rule induction | W4.1–4.4, P21.1 | [ PDF | LaTeX ] | |
| 8 | 15 | Evaluation contexts | [ PDF | LaTeX ] | ||
| Language Features | |||||
| 9 | 18 | Semantics via translation | [ PDF | LaTeX ] | ||
| 10 | 20 | uML, strong typing, scope | [ PDF | LaTeX ] | ||
| 11 | 22 | Computing with Closures | TG7 | [ PDF | LaTeX ] | |
| 12 | 25 | Modules and State | TG8 | [ PDF | LaTeX ] | due: PS2 |
| 13 | 27 | Predicate transformers | Predicate Transformers (Dijkstra) (W6) | [ PDF | LaTeX ] | |
| 14 | 29 | Weakest liberal preconditions, Hoare logic | 10 Years of Hoare's Logic, §1,2 (Apt), (W7) | [ PDF | LaTeX ] | handout: PS3 |
| 15 | Oct 2 | Semantics and completeness of Hoare logic | Notes on propositional Hoare logic (Tiuryn) | [ PDF | LaTeX ] | |
| 16 | 4 | Kleene algebra and Dynamic Logic | [ PDF | LaTeX ] | ||
| 17 | 6 | CPS conversion | [ PDF | LaTeX ] | ||
| 9 | No class: fall break | ||||
| 18 | 11 | Continuations and exceptions | [ PDF | LaTeX ] | ||
| Denotational (Fixpoint) Semantics | |||||
| 19 | 13 | Denotational semantics of IMP | W5.1–5.2 | [ PDF | LaTeX ] | |
| 20 | 16 | Metalanguage and domain constructions | W5.3–5.4, W8.1–4 | [ PDF | LaTeX ] | |
| 21 | 18 | Denotational semantics of REC | W9.1–3,5–6 | [ PDF | LaTeX ] | |
| 22 | 20 | Scott's Dinfinity construction | Lambda-logic (Rudin) | [ PDF | LaTeX ] | due: PS3 |
| Static Semantics | |||||
| 23 | 23 | Typed lambda calculus | P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 | [ PDF | LaTeX ] | handout: PS4 |
| Oct 24 | Prelim, 7:30–9:30pm, Upson 205 | See CMS for sample prelim | |||
| 24 | 25 | Soundness of the typing rules | P8.3, P9.3, (W11.9) | [ PDF | LaTeX ] | |
| 25 | 27 | Products, sums, and other data types | P11.1–10, (W11.11) | [ PDF | LaTeX ] | |
| 30 | Continuation of last class | ||||
| 26 | Nov 1 | Strong Normalization | P12, (W11.4–8) | [ PDF | LaTeX ] | |
| 3 | No class | ||||
| 27 | 6 | Type inference and unification | P22.1–5 [typeCheck.sml] | [ PDF | LaTeX ] | |
| 28 | 8 | The Polymorphic Lambda-Calculus | P22.6–7, P23 | [ PDF | LaTeX ] | |
| 29 | 10 | Continuation of last class | |||
| 30 | 13 | Propositions as Types | Wadler | [ PDF | LaTeX ] | due: PS4 |
| 31 | 15 | Continuation of last class | handout: PS5 | ||
| 32 | 17 | Propositions as Types, continued | KAT interactive theorem prover | [ PDF | LaTeX ] | |
| 33 | 20 | Subtype Polymorphism | P15.1–6, G9 | [ PDF | LaTeX ] | |
| 34 | 22 | Recursive Types | P20, W13, G5,10 | [ PDF | LaTeX ] | |
| 24 | No class: Thanksgiving break | ||||
| 35 | 27 | Equality and Subtyping of Recursive Types | [ PDF | LaTeX ] | ||
| 36 | 29 | Type Inference for Partial Types | [ PDF | LaTeX ] | ||
| 37 | Dec 1 | Abstract Interpretation | [ PDF | LaTeX ] | ||
| Dec 4 | due: PS5 | ||||
| Dec 8 | Final Exam, 2–4:30pm, Hollister 306 | See CMS for sample final | |||
P = Pierce, W = Winskel, TG = Turbak & Gifford, M = Mitchell, AC = Abadi & Cardelli, G = Gunter