CS 611 Schedule

This 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


Key to Readings

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.