CS 611 Fall 2007 Schedule

The future is subject to change, and the past may require correction. Lecture notes have been updated through lecture 40. If you spot any problems with the notes, your corrections or suggestions are appreciated.

# Date Topic Readings* Lecture notes (=slides) Homework
Operational semantics and proof techniques
1 Aug. 24 Course introduction P1,2 PDF ] handout: PS1 (Part 3)
2 27 Lambda calculus P5.1–5.2 PDF | LaTeX ]
3 29 Lambda calculus encodings and recursion P5.3–5.4 PDF | LaTeX ]
4 31 Normal forms P3.1,3.2,3.4,3.5 PDFLaTeX ]
5 Sept. 3 Big-step vs. small-step SOS P3.3,3.6,W2 PDFLaTeX ]
6 5

Well-founded induction and function definitions

W3.1–3.3 PDFLaTeX ] due: PS1
handout: PS2
7 7 Inductive definitions and rule induction W4.1–4.4, P21.1 PDFLaTeX ]
8 10 Evaluation contexts   PDFLaTeX ]
Language features and translations
9 12 Semantics via translation   PDFLaTeX ]
10 14 uML, strong typing, scope   PDFLaTeX ] due: PS2a
handout: PS3
11 17 Naming (Lecturer: Steve Chong)   PDFLaTeX ]
12 19 Closures (Lecturer: Dexter Kozen)   PDFLaTeX ]
13 21 Modules and state   PDFLaTeX ] due: PS2b
14 24 State and mutable variables   PDFLaTeX ]
15 26 Continuation-passing style and CPS conversion   PDFLaTeX ]
16 28 Nonlocal control: errors and exceptions   PDFLaTeX ] due: PS3
17 Oct. 1 First-class continuations, compiling with continuations   PDFLaTeX ] handout: PS4
Axiomatic semantics
18 3 Hoare logic 10 Years of Hoare's Logic, §1,2 (Apt), (W6)  (No notes; read Winskel.)
19 5 Weakest preconditions Predicate Transformers (Dijkstra) (W7)
8

No class: fall break

Denotational (fixed-point) semantics
20 10 Denotational semantics of IMP W5.1–5.2 PDFLaTeX ]
21 12 The Fixed-Point Theorem W5.3–5.4 PDFLaTeX ]
22 15 Domain constructions (Lecturer: Dexter Kozen) W8.1–4 PDFLaTeX ]
23 17 Metalanguage for denotational semantics (Lecturer: Dexter Kozen)
24 19 Denotational semantics of functions W9.1–3,5–6 PDFLaTeX ] due: PS4
25 22 Solving domain equations W12, M7, Gunter 5, 9 PDFLaTeX ]
Oct. 23 Prelim, 7:30–9:30PM, Upson 109. Covers lectures 1–24 (incl. REC semantics) See CMS for sample prelim
Static semantics (type systems)
24 No class (post-exam)
26 26 Simply-typed lambda calculus P8.1–2, P9.1–2, P9.5–9.6, P10.1–3, W11.1–3 PDFLaTeX ]
27 29 Products, sums, and more P11.1–10, (W11.11) PDFLaTeX ] handout: PS5 (q3)
28 31 Soundness of the type system P8.3, P9.3, (W11.9) PDFLaTeX ]
29 Nov. 2 Logical relations and strong normalization P12, (W11.4–8) PDFLaTeX ]
30 5 Recursive types P20, W13 (Gunter 5, 10) PDFLaTeX ]
31 7 Subtype polymorphism
(Lecturer: Radu Rugina)
P15.1–6 (Gunter 9) PDFLaTeX ]
32 9 Type inference P22.1–5 PDFLaTeX ]
33 12 Parametric polymorphism P22.6–7, P23 PDFLaTeX ]
34 14 Recitation due: PS5
35 16 Propositions as types Wadler PDFLaTeX ] handout: PS6
36 19 Existential types P24–24.2 CW86 (Mitchell 9.4–9.5) PDFLaTeX ]
37 21 Parameterized types and higher-order polymorphism P29–30 PDF (2005) | LaTeX ]
23 No class: Thanksgiving break
38 26 Object-oriented languages P18, (AC 1-4)
39 28 Object calculi and encodings (AC 5–8)
40 30 Bounded quantification and directions in PL research P26, (MLB97, M99, ZCMZ03, NCM04, LM06) due: PS6
Dec. 12 Final Exam, 7:00–9:30pm, Hollister 362

Key to Readings

P = Pierce, W = Winskel, M = Mitchell, AC = Abadi & Cardelli