|
| Meeting | Date | Topic | Reading | Scribe | Handout | Due | ||
|---|---|---|---|---|---|---|---|---|
Dynamic semantics and proof techniques |
||||||||
| 1 | Aug. 27 | Course overview, IMP | Ch. 1 | Maasha | ||||
| 2 | 30 | Introduction to SML | Paulson or Harper | |||||
| 3 | Sept. 1 | Operational semantics, equivalence | 2.1-2.3 | Yoon [ps] | ||||
| 4 | 3 | Interpretation, more lang. features | 2.4-2.5 | Chen | HW1 | |||
| 5 | 6 | Small-step semantics & induction | 2.6, 3.1-3.5 | Myers [ps] | ||||
| 6 | 8 | Rule induction | 4.1-4.2 | Myers [ps] | ||||
| 10 | No class |
|||||||
| 7 | 13 | More proof techniques | 4.3-4.4 | Fluet | HW1 | |||
| 8 | 15 | Untyped lambda calculus | Myers [ps] | |||||
| 9 | 17 | Recursion, scope, substitution | Myers [ps] | HW2 | ||||
| 10 | 20 | Reduction orders, normal form | Myers [ps] | |||||
| 11 | 22 | Denotational semantics | 5.1-5.2 | Myers [ps] | ||||
| 12 | 24 | Fixed points and cpo's | 5.3-5.4 | Nystrom | ||||
| 13 | 27 | The fixed point theorem | 8.1-8.2 | Faradjian | ||||
| 14 | 29 | Domain theory | 8.3-8.4 | |||||
Language features |
||||||||
| 15 | Oct. 1 | Parameter passing | 9.1-9.6 | Kliger | ||||
| 16 | 4 | Recursion | 9.7-9.8 | Fleming | HW3 | HW2 | ||
| 17 | 6 | Lazy functional language, scope | Myers | |||||
| 18 | 8 | State: operational semantics | Marques | |||||
| 11 | No class: Fall Break |
|||||||
| 19 | 13 | State: variables, pass by reference | Welte | |||||
| 20 | 15 | Control: standard semantics | Faradjian | |||||
| 21 | 18 | Control: non-local transfers | Harris | HW3 | ||||
| 22 | 20 | Semantics to code: pragmatics | Myers [ps] | |||||
| 23 | 22 | In-class prelim |
||||||
Static Semantics |
||||||||
| 24 | 25 | Axiomatic semantics | 6.1-6.6 | Wang | ||||
| 25 | 27 | Axiomatic semantics: soundness | 7.1-7.2 | Liang | ||||
| 26 | 29 | Weakest preconditions | 7.3-7.4 | Ramasubramanian | ||||
| 27 | Nov. 1 | Simply-typed lambda calculus | 11.1-11.3 | Kolmogorov | HW4 | |||
| 28 | 3 | Soundness of typing rules | Chandra, Liang | |||||
| 29 | 5 | Adequacy, strong normalization | 11.4-11.7 | Myers [ps] | ||||
| 30 | 8 | More types | 11.9, 11.11 | Samuels | ||||
| 31 | 10 | Recursive types and domains | 13.1-13.2, (Gunter 7.4) |
Myers [ps] | ||||
| 32 | 12 | Type inference, ML (predicative) polymorphism | Swamy | HW5 | HW4 | |||
| 33 | 15 | More parametric polymorphism | (Gunter, Ch.11) | Myers [ps], Chandra | ||||
| 34 | 17 | Curry-Howard isomorphism | Woo | |||||
| 35 | 19 | Subtype polymorphism | (Gunter, Ch. 9) | Rama, Nystrom | ||||
| 36 | 22 | Records and existential types | (Mitchell, 9.4) | Wang, Chen | ||||
| 37 | 24 | Modules and objects | Harris | HW6 | HW5 | |||
| 26 | No class: Thanksgiving Break |
|||||||
| 38 | 29 | Objects: classes, advanced features (A&C, Ch.1-6) | Nystrom | |||||
| 39 | Dec. 1 | Object types (Abadi &Cardelli, Ch. 7-9) | Zheng, Swamy | |||||
| 40 | 3 |
|
HW6 | |||||
41 |
Dec. 15 | Final Exam (3:00-5:30PM) |
||||||
