CS 611 ScheduleThis schedule is subject to change and is only intended as a rough guide at present. |
|||||
# | 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.