|
||||||
| # | Date | Topic | Readings* | Scribe  =slides |
Homework | |
|---|---|---|---|---|---|---|
|
Operational semantics and proof techniques | ||||||
| 1 | Aug. 31 | Course overview, IMP | W1, P2, P3.1-3.2, T&G A.1 | Ananthakrishna, Singh | ||
| 2 | Sep. 3 | Large-step semantics | W2.1-3 | Niculescu-Mizil, Petride | ||
| 3 | 5 | Small-step semantics | W2.4-6 | Brukman, Kamzyuk | handout: HW1 | |
| 4 | 7 | Introduction to Caml (Grossman) | Introduction to Objective Caml | Grossman (zip file) | ||
| 5 | 10 | Inductive proofs | W3.1-5, P3.3-3.6 | Zatsman, Liu | ||
| 6 | 12 |
Inductive definitions |
W4.1-4 | Chong, Linga | ||
| 7 | 14 | Lambda calculus | P5.1-5.2, T&G A.2 | Breck, Hartline | ||
| 8 | 17 | Lambda calculus encodings |
P5.3-5.4, T&G 8.2-3 |
Guo, Shao | due: HW1 | |
| 9 | 19 | Substitution, reductions, normal form | Milanovici, Montalban | handout: HW2 | ||
| 10 | 21 | Evaluation contexts | Sharp, Chung | |||
| Language features | ||||||
| 11 | 24 | Definitional translation | T&G 9.1 | Chao, Niculescu-Mizil | ||
| 12 | 26 | uF, recursive fns, naming & scope | T&G 9.2.1 | Singh, Anantakrishna | ||
| 13 | 28 | Naming and state | T&G 10.1-2 | Petride | ||
| 14 | Oct. 1 | Imperative features, continuation-passing style | T&G 10.3 | Zhang, Capobianco | due: HW2 | |
| 15 | 3 | Control: CPS semantics | T&G 11.1-2 | Yeh, Chang | handout: HW3 | |
| 16 | 5 | Control: exceptions and more | T&G 11.3-5 | McCloskey, Chao | ||
| 8 |
No class: fall break |
|||||
| Denotational (fixed-point) semantics | ||||||
| 17 | 10 | Denotational semantics of IMP | W5.1-2 | Anantakrishna, Singh | ||
| 18 | 12 | Fixed points and cpo's | W5.3-4 | Hardin, Clarkson | ||
| 19 | 15 | Fixed Point Theorem | W8.1-2 | Schuller, Gabay | ||
| 20 | 17 | Domain constructions | W8.3-4, T&G A.3 | Kifer, Wang |
||
| 21 | 19 | Denotational semantics of REC | W9.1-3,5-6, T&G 9.1 | Pang, Nagarajan | ||
| 22 | 22 | Axiomatic Semantics | Hoare logic (Kozen) | W7.2, 7.5 | Ragheb, Sharp
|
due: HW3, handout: HW4 |
| 23 | 24 | Kleene Algebra with Tests (Kozen) | no scribe |
|||
| 24 | 26 | Domain equations: uF semantics | W9.4,7 | Breck, Kim (2000: Hardin, Wang) | ||
| 25 | 29 | Standard semantics, non-hierarchical scope | Myers | due: HW4 | ||
|
Static semantics | ||||||
|
26 |
31 |
Prelim review (Nystrom, Wang) |
||||
|
Nov. 1 |
Preliminary Exam 7:30–9:30PM, Upson 205. Covers lectures 1–22, 24–25. |
|||||
|
2 |
No class: post-exam |
|||||
| 28 | 5 | Typed lambda calculus | P8.1-2, P9.1-2, P10.1-3 (W11.1-3) | Meyerguz (Myers) | ||
| 29 | 7 | Soundness of typing rules | P11.1-10, W11.9, W11.11 | Chong, Linga | ||
| 30 | 9 | Products, sums, and more | W11.11, (Gunter 7.4) | Montalban, Zhang | handout: HW5 | |
| 31 | 12 | Logical relations: strong normalization | P12, W11.4–8 | Chung, McCloskey | ||
| 32 | 14 | Isorecursive types | P20, W13 (Gunter 5, 10) | Guo, Shao | ||
| 33 | 16 | Equirecursive types, recursive domains | P21, W12.1–5, T&G 13.7 | Liu, Kim | ||
| 34 | 19 | More recursive domains, type inference | P22, (T&G 13.6, Gunter 7.5) | |
||
| 35 | 21 | Parametric polymorphism | P23, (Gunter 11.1) | Zatsman | ||
| 23 | No class: Thanksgiving break | |||||
| 36 | 26 | The Curry–Howard isomorphism | Wadler | Capobianco, Chang (draft) | due: HW5, handout: HW6 | |
| 37 | 28 | Subtype polymorphism | P15, (Gunter 9) | |||
| 38 | 30 | Subtyping, existential types | CW86, P24, (Mitchell 9.4) | Yeh, Chao | ||
| 39 | Dec. 3 | Encoding modules | (Mitchell 9.5) | Montalban, Zhang (draft) | ||
| 40 | 5 | Classes, inheritance, constructors | JLS, (A&C 1–6) | |
||
| 41 | 7 | Parameterized types and more | BCP97, P26,29,30 (A&C 7–8) | |
due: HW6 | |
|
19 |
Final Exam 9:00–11:30AM, Olin 245 |
|||||
W = Winskel, T&G = Turbak & Gifford, M = Mitchell, A = Abadi & Cardelli
