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. 26 Course introduction P1,2 Ravikant Dintyala [ PDF | LaTeX ] handout: PS1
2 29 Lambda calculus P5.1–5.2 Oliver Kennedy [ PDF | LaTeX ]
3 31 Lambda calculus encodings and recursion P5.3–5.4 Bryant Adams [ PDF | LaTeX ]
4 Sep. 2 Normal forms P3.1,3.2,3.4,3.5 Ymir Vigfusson, Daria Sorokina [ PDF | LaTeX ]
  5 No class: Labor Day
5 7 Big-step vs. small-step SOS (Radu Rugina) P3.3,3.6,W2 Jon Guarino, Kevin Markman [ PDF | LaTeX ] due: PS1
6 9

Well-founded induction and function definitions

 W3.1–3.3 James Worthington, Soam Vasani [ PDF | LaTeX ] handout: PS2
7 12 Inductive definitions and rule induction W4.1–4.4, P21.1 Yisong Yue, Yunsong Guo [ PDF | LaTeX ]
8 14 Evaluation contexts   Georgios Piliouras, Raghu Ramanujan [ PDF | LaTeX ]
Language features
9 16 Semantics via translation   Olga Belomestnykh [ PDF | LaTeX ]
10 19 uML, strong typing, scope   Nam Nguyen, Lukas Kroc [ PDF | LaTeX ]
11 21 Naming TG7 Yookyung Jo, Lars Backstrom [ PDF | LaTeX ]
12 23 State TG8 Jon Guarino, Kevin Markman [ PDF | LaTeX ] due: PS2
13 26 Predicate transformers (Michael Clarkson) Predicate Transformers (Dijkstra) (W6) Asif-ul Haque, Ryan Peterson [ PDF | LaTeX ]

Axiomatic semantics
14 28 Mutable variables, objects (AC1–6) Michael O'Connor, Mia Minnes [ PDF | LaTeX ] handout: PS3
15 30 Hoare logic (Michael Clarkson) 10 Years of Hoare's Logic, §1,2 (Apt), (W7) Bryant Adams, Mia Minnes [ PDF | LaTeX ] Axiomatic semantics
16 Oct. 3 Control and CPS   2004 notes [ PDF ]
17 5 CPS semantics and exceptions   Wyatt Schweizer, David Crandall [ PDF | LaTeX ]
18 7 In-class recitation: PS2 review (Mike George)    
10

No class: fall break
Denotational (fixed-point) semantics
19 12 Denotational semantics of IMP W5.1–5.2 Mia Minnes, James Worthington [ PDF | LaTeX ]
20 14 The fixed point theorem W5.3–5.4 2004 notes covering lectures 19,20 [ PDF | LaTeX ]
21 17 Metalanguage and domain constructions W8.1–4 Michael O'Connor. [ PDF | LaTeX | 2004 ]
22 19 Denotational semantics of REC W9.1–3,5–6 Bryant Adams, Olga Belomestnykh [ PDF | LaTeX ]
Oct. 20 Prelim, 7:30–9:30PM, Phillips 307. Covers lectures 1–21 See CMS for sample prelim
21 No class (post-exam)
Static Semantics
23 24 Typed lambda calculus P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 2004 notes [ PDF | LaTeX ] handout: PS4
24 26 Soundness of typing rules P8.3, P9.3, (W11.9) 2004 notes [ PDF | LaTeX ]
25 28 Products, sums, and more P11.1–10, (W11.11) David Crandall, Lukas Kroc [ PDF | LaTeX ]
26 31 Logical relations and strong normalization P12, (W11.4–8) Michael O'Connor, Jeffery Zhang [ PDF | LaTeX ]
27 Nov. 2 Type inference P22.1–5
28 4 Parametric polymorphism P22.6–7, P23 Ryan Peterson, Kevin Markman [ PDF | LaTeX ]
29 7 Standard semantics and first-class continuations   Yisong Yue [ PDF | LaTeX ]
30 9 Types as propositions Wadler Mia Minnes, Nam Nguyen [ PDF | LaTeX ] due: PS4
31 11 Subtype polymorphism (Radu Rugina) P15.1–6 (Gunter 9) Georgios Piliouras, Raghuram Ramanujam [ PDF | LaTeX ] handout: PS5
32 14 Recursive types P20, W13 (Gunter 5, 10) Xin Zheng, Asif-ul Haque [ PDF | LaTeX ]
33 16 Coercion functions, recitation (Mike George)   2004 notes [ PDF ]
  18 No class: makeup lecture 11/28,11/29  
34 21 Equirecursive types, domain equations    
35 23 Existential types P24–24.2 2004 notes [ PDF | LaTeX ]
25 No class: Thanksgiving break
36 28 Modules and dependent types CW86, P24 (Mitchell 9.4–9.5) Yookyung Jo, Aaron Lenfestey [ PDF | LaTeX ]
37 28/29 Parameterized types P29, P30.5
(Monday: Ph307, Tuesday: Hollister 312)		 David Crandall, Yookyung Jo [ PDF | LaTeX ]
38 30 Object-oriented languages P18, (AC 1-4)
39 Dec. 2 More OO: beyond classes (AC 6-8) due: PS5
Dec. 8 Final Exam, 9:00–11:30am, Olin 245

Key to Readings

P = Pierce, W = Winskel, TG = Turbak & Gifford (selected chapters available from Bill Hogan), M = Mitchell, AC = Abadi & Cardelli