CS 6110 (Spring 2011)
Advanced Programming Languages
MWF 10:10-11:00
Phillips 213
Schedule
This schedule is not set in stone. Changes will be announced in lecture and posted here. Please check back from time to time.
Readings key: W = Winskel, P = Pierce.
| Date | Topic | Notes | Reading | Assignments |
| 24 Jan | Introduction | notes slides |
P1-2 | |
| 26 Jan | λ-calculus, substitution | notes | P5.1,5.3 | |
| 28 Jan | λ-calculus reduction, confluence, and Church encodings | notes handout |
P5.2 | |
| 31 Jan | Reduction Strategies and Equivalence | notes | P5.2 | |
| 2 Feb | Cornell closed due to weather (no class) | HW1 out | ||
| 3 Feb | OCaml Recitation — 7:30pm in Upson B7 | slides source |
||
| 4 Feb | Recursion and fixed point combinators | notes | P5.2 | |
| 7 Feb | Structured Operational Semantics and IMP | notes | W2 | |
| 9 Feb | Well-founded induction | notes | W3.1-3.2 | |
| 11 Feb | Inductive definitions and least fixed points | notes | W3.3-3.5, W4 | |
| 14 Feb | Evaluation contexts | notes | ||
| 16 Feb | Definitional Translation | notes | HW1 due HW2 out |
|
| 18 Feb | FL and strong typing | notes slides |
||
| 21 Feb | Naming and scope | notes | ||
| 23 Feb | Recursive bindings and modules | notes | ||
| 25 Feb | State and mutable variables | notes | ||
| 28 Feb | Continuations | notes | ||
| 2 Mar | Exceptions and first-class continuations | notes | HW2 due | |
| 4 Mar | Compiling with continuations | notes | HW3 out | |
| 4 Mar |
FastTrack and Jumble: Efficient and Precise Dynamic Detection of Data Races Stephen Freund — 12pm in Upson 315 |
|||
| 7 Mar | PhD Open House (no class) | |||
| 9 Mar | Predicate Transformers | notes | W6.1-6.3 | |
| 11 Mar | Hoare Logic | notes handout |
W6.4-6.6, W7 | |
| 14 Mar | Denotational semantics of IMP | notes | W5 | |
| 16 Mar | The Fixed-Point Theorem | notes | W8 | |
| 18 Mar | Domain Constructions | notes | W8 | HW3 due |
| 21 Mar | Spring break (no class) | |||
| 23 Mar | Spring break (no class) | |||
| 25 Mar | Spring break (no class) | |||
| 28 Mar | Review | |||
| 30 Mar | Preliminary Exam | |||
| 1 Apr | Denotational semantics for REC | notes | W9 | |
| 4 Apr | Scott's D-∞ construction | notes | W12 | HW4 out |
| 6 Apr | Typed λ-calculus | notes | P9 | |
| 8 Apr | Type soundness | notes | P8 | |
| 11 Apr | Products, Sums, and Recursion | notes | P11 | |
| 13 Apr | Subtyping | notes | P15 | |
| 15 Apr | Algorithmic Subtyping and Type Inference | notes | P16, P22 | HW4 due |
| 18 Apr | Polymorphism | notes | P23 | HW5 out |
| 20 Apr | Strong normalization and logical relations | notes | P12 | |
| 22 Apr | Propositions as types | notes | P9.4 | |
| 25 Apr | Recursive types | notes | P20 | |
| 27 Apr | Equirecursive equality | notes | P21 | HW5 due HW6 out |
| 29 Apr | Existential types | notes | P24 | |
| 2 May | Object encodings | paper | P18, 24.2 | |
| 4 May | Monads | notes | Moggi Wadler |
|
| 6 May | Current Research in Programming Languages | HW6 due | ||
| 9 May | Study Period (no class) | |||
| 11 May | Study Period (no class) | |||
| 13 May | Final Exam (2:00-4:30pm) | |||
