|
||||||
| # | Date | Topic | Reading | Scribe  =slides |
Handout | Due |
|---|---|---|---|---|---|---|
Dynamic semantics | ||||||
| 1 | Aug. 25 | Course overview, IMP | Ch. 1, T&G A.1 | Weissman, Marques |
||
| 2 | 28 | Large-step semantics | 2.1-3 | Weissman, Marques | ||
| 3 | 30 | Small-step semantics | 2.4-6 | Das, Fernandes | ||
| 4 | Sep. 1 | Introduction to ML (Fluet) | Paulson or Harper | no scribe | HW1 | |
| 5 | 4 | Inductive proofs | 3.1-5 | no scribe |
||
| 6 | 6 | Inductive definitions |
4.1-4 | Gale, Dasgupta |
||
| 7 | 8 | Lambda calculus | T&G A.2 | Bronevetsky, Anshelevich
|
||
| 8 | 11 | Recursion, scope, substitution |
T&G 8.2-3 |
O'Neill, Wexler |
HW2 | HW1 |
| 9 | 13 | Reductions and normal form | Gale, Dasgupta |
|||
| 10 | 15 | Denotational semantics | 5.1-2 | Patron, Shontz |
||
| 11 | 18 | Fixed points and cpo's | 5.3-4 | Hardin, Clarkson |
||
| 12 | 20 | The Fixed Point Theorem | 8.1-2 | Schuller, Gabay | ||
| 13 | 22 | Domain constructors | 8.3, T&G A.3 | Kifer, Y. Wang |
||
| 14 | 25 | A meta-language | 8.4 | Gleason, Pal
|
HW2 | |
Language features | ||||||
| 15 | 27 | Parameter passing | 9.1-3, 9.5-6, T&G 9.1 | HW3 | ||
| 16 | Sep. 29 | Operational vs. denotational semantics | 9.4, 9.7 | |||
| 17 | Oct. 2 | uF semantics, scope | T&G 9.2 | Hardin, K. Wang | ||
| 18 | 4 | Call-by-name uF | T&G 10.1-2 | Qiu, Yao | ||
| 19 | 6 | Modeling state | T&G 10.3 | |||
|
9 |
No class: Fall Break |
|||||
| 20 | 11 | Axiomatic semantics/Hoare logic (Kozen) | 6.1-6 | Pang, Das | ||
| 21 | 13 | Kleene Algebra with Tests (Kozen) | 7.2, 7.5 | Schuller, Wexler |
HW4 | HW3 |
| 22 | 16 | Continuation-passing style | Anshelevich, Bronevetsky | |||
| 23 | 18 | CPS semantics | T&G 11.1-2 | Yotov, Fernandes | ||
| 24 | 20 | Non-local control, exceptions | T&G 11.3-5 | Bucila, Costea | ||
Static semantics | ||||||
| 25 | 23 | Typed lambda calculus | 11.1-3, (Gunter 2.1-2) | Meyerguz | HW4 | |
|
26 |
25 |
Prelim review (Fluet, Cheney) |
no scribe | |||
|
26 |
Preliminary Exam 7:30-9:30PM, Stimson G1 (covers lectures 1-24) |
|||||
|
27 |
No class |
|||||
| 27 | 30 | Soundness of typing rules | Y. Wang, Kifer | |||
| 28 | Nov. 1 | Logical relations, strong normalization | 11.4-7 | Proskourine, Harren |
||
| 29 | 3 | Products, sums, and more | 11.9, 11.11 | Kobyakov, Malesevic | ||
| 30 | 6 | Recursive types | 12.1-2, 13.1-2, (Gunter 7.4) |
Shontz, Patron |
||
| 31 | 8 | Recursive domains | 12.3-5, (Gunter 5, 10) | no scribe |
HW5 | |
| 32 | 10 | Type inference, ML polymorphism | T&G 13.7, (Gunter 7.5) | Williams, Nagarajan |
||
| 33 | 13 | Parametric polymorphism | T&G 13.6 (Gunter 11.1) | Gleason, Yotov |
||
| 34 | 15 | Curry-Howard isomorphism | Wadler/DDJ | O'Neill, Kobyakov | ||
| 35 | 17 | Subtype polymorphism | (Gunter 9) | Clarkson, Proskourine | ||
| 36 | 20 | Subtyping, existential types | CW86, (Mitchell 9.4) | Rajagopalan, Gabay | HW6 | HW5 |
| 37 | 22 | Module types | (Mitchell 9.5) | Liu, Bray
|
||
|
24 |
No class: Thanksgiving Break |
|||||
| 38 | 27 | Objects | JLS, (A&C 1-6) | Sandler, Malesevic | ||
| 39 | 29 | More objects | BCP97, (A&C 7-8) | Allevena, Slivkins (draft) |
||
| 40 | Dec. 1 | Objects and parameterized types | no scribe |
HW6 | ||
Dec. 7 |
Final Exam 12:00-2:30PM, Phillips 101 |
|||||
