CS 611 Schedule |
||||||
# | 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 |