CS 611 Schedule
This schedule is subject to change and is only intended as a rough guide at present.
=slidesWell-founded induction
No class: fall break
|
|||||
| # | Date | Topic | Readings* | Scribe =slides |
Homework |
|---|---|---|---|---|---|
| Operational semantics and proof techniques | |||||
| 1 | Aug. 30 | Course overview, lambda calculus | P1,2; Wojtek's Crash course on SML | ||
| 2 | Sep.1 | Lambda calculus encodings | P5.1–5.2 | Lucja Kot, Hitesh Ballani | |
| 3 | 3 | Recursion, substitution | P5.3–5.4 | Helgi Ingolfsson, Yoni Ben-Simhon | handout: PS1 |
| 4 | 6 | Reductions and normal forms | P3.1,3.2,3.4,3.5 | Sam Arbesman, Muthu Venkitasubramaniam | |
| 5 | 8 | Big-step vs. small-step SOS | P3.3,3.6,W2 | Arjun Rao, Matthew Stedinger | |
| 6 | 10 |
Well-founded induction |
W3.1–3.3 | ||
| 7 | 13 | Inductive definitions | W4.1–4.4, P21.1 | Dan Stowell, Shafquat Rahman | |
| 8 | 15 | Rule induction, evaluation contexts | Lucja Kot, Michael George | due: PS1 | |
| Language features | |||||
| 9 | 17 | Semantics via translation | TG 6 | Dan Sheldon, Maksim Orlovich | |
| 10 | 20 | Recursive functions, naming, scope | TG 7 | Yogi Sharma, Bryan Silverthorn | handout: PS2 |
| 11 | 22 | Modules, State. | TG 8 | K. Vikram, David Crandall | |
| 12 | 24 | Mutable variables | Krzysztof Ostrowski, Yejin Choi | ||
| 13 | 27 | CPS conversion and control | TG 9 | Ian Kash, Yee Jiun Song | |
| 14 | 29 | Exceptions and continuations | Mike Jennings, Jonathan Kaldor | ||
| 15 | Oct. 1 | Compiling with continuations | Yogi Sharma, Shafquat Rahman | ||
| Denotational (fixed-point) semantics | |||||
| 16 | 4 | Denotational semantics of IMP | W5.1–5.2 | Notes | due: PS2 |
| 17 | 6 | The fixed point theorem | W5.3–5.4 | Notes | handout: PS3 |
| 18 | 8 | Metalanguage and domain constructions | W8.1–4 | Yee Jiun Song, Dan Stowell | |
| 10 |
No class: fall break |
||||
| 19 | 13 | Denotational semantics of REC | W9.1–3,5–6 | Grant Goodale, Liviu Popescu (related notes from 2001) | |
| 20 | 15 | Denotational semantics of uML | Ian Kash, Jonathan Kaldor | ||
| 21 | 18 | Prelim review | due: PS3 | ||
| 19 | Prelim, 7:30–9:30PM, Phillips 219. Covers lectures 1–20 | See CMS for sample prelim | |||
| 20 |
No post-exam class meeting | ||||
| Static Semantics | |||||
| 22 | 22 | Typed lambda calculus | P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 | Notes | |
| 23 | 25 | Soundness of typing rules | P8.3, P9.3, (W11.9) | Notes | |
| 24 | 27 | Products, sums, and more | P11.1–10, (W11.11, Gunter 7.4) | Notes | Handout: PS4 |
| 25 | 29 | Logical relations and strong normalization | P12, (W11.4–8) | Patrick Ng, Muthu Venkitasubramaniam | |
| 26 | Nov. 1 | Type inference | P22.1–5, (TG 13.6, Gunter 7.5) | Slides | |
| 27 | 3 | Let-polymorphism | P22.6–7, (Gunter 11.1) | Slides | |
| 28 | 5 | More type parameterization | P23,29,30-30.4 | Slides | due: PS4 |
| 29 | 8 | Types as propositions | Wadler | Mike George, K. Vikram | |
| 30 | 10 | Recursive types | P20, W13 (Gunter 5, 10) | Arjun Rao, Yogeshwer Sharma | |
| 31 | 12 | Subtype polymorphism | P15.1–6, (Gunter 9) | Helgi Ingolfsson, Shobhit Varshney | |
| 32 | 17 | Equirecursive types | (P21) | John Yu, Dan Sheldon | handout: PS5 |
| 33 | 19 | Existential types | P24-24.2 | Maksim Orlovich, Sam Arbesman | |
| 34 | 22 | Modules and dependent types | P24, P30.5 (M9.4–9.5, CW86) | Liviu Popescu | due: PS5 |
| 35 | 23 | Object-oriented languages | P18, (AC 1–6) | Slides | handout: PS6 |
| 36 | 24 | Object calculus, bounded polymorphism, mixins |
P19, P32, (AC 7-8) | Slides | |
| 26 | No class: Thanksgiving break | ||||
| Axiomatic Semantics | |||||
| 37 | 29 | Hoare logic (axiomatic semantics) | W6 | Yejin Choi, Bryan Silverthorn (draft) | |
| 38 | Dec. 1 | Weakest preconditions, verification conditions | W7.1-7.2, 7.4 | Helgi Ingolfsson, Yoni Ben-Simhon | |
| 39 | 3 | Abstract interpretation | Krzysztof Ostrowski | due: PS6 | |
| Dec. 15 | Final Exam, 3:00–5:30pm, Hollister 206 | ||||
P = Pierce, W = Winskel, TG = Turbak & Gifford, M = Mitchell, AC = Abadi & Cardelli
Most readings are required readings; parenthesized readings are places to get extra detail or another viewpoint.