CS 6110 (Spring 2016)
Advanced Programming Languages
MWF 10:10-11:00
Gates 114
Schedule
Key: P = Pierce, W = Winskel
| Date | Topic | Notes | Reading | Assignments |
| 27 January | Overview | slides notes | P 1-5 | |
| 29 January | λ-calculus | notes extra | P 5 | |
| 1 February | λ-calculus encodings | notes | P 5 | HW1 out |
| 3 February | Reduction strategies and eqivalence | notes | P 5 | |
| 5 February | Observational equivalence | notes | P 5 | |
| 8 February | Fixpoints | notes | P 5 | |
| 10 February | Well-Founded Induction | notes | W 3, 4 | |
| 12 February | Inductive Definitions and Leatst Fixpoints | notes | W 3, 4, 5.5 | HW 1 due |
| 15 February | No class (February break) | |||
| 17 February | The IMP Language | notes | W 2 | HW 2 out |
| 19 February | Semantics via Translation | notes | ||
| 22 February | Adequacy | notes | ||
| 24 February | A Functional Language | notes | P 11 | |
| 24 February | Scope | notes | ||
| 29 February | State | notes | P 13 | |
| 2 March | Continuations | notes | HW2 due; HW3 out | |
| 4 March | Exceptions and First-class Continuations | notes | ||
| 7 March | Axiomatic Semantics and Hoare Logic | notes | ||
| 9 March | Kleene Algebra with Tests | notes | ||
| 11 March | Predicate Transformers | notes | W 7 | Guest lecture: Fran Mota |
| 14 March | Denotational Semantics | notes | W 5 | Guest lecture: Greg Morrisett |
| 16 March | CPOs | notes | W 8 | |
| 18 March | Domain Constructions | notes | HW 3 due | |
| 21 March | Denotational Semantics for FL | notes | ||
| 23 March | Preliminary Exam | |||
| 25 March | Scott's D-∞ construction | notes | ||
| 28 March | No class (Spring Break) | |||
| 30 March | No class (Spring Break) | |||
| 1 April | No class (Spring Break) | |||
| 4 April | Prelim Debrief | HW 4 out | ||
| 6 April | Typed λ-calculus | notes | P 9 | |
| 8 April | Type Soundness | notes | P 9 | |
| 11 April | Products, Sums, and Datatypes | notes | P 11 | |
| 13 April | Products, Sums, and Datatypes, cont'd | notes | P 11 | |
| 15 April | Strong Normalization | notes | P 12 | HW 4 due |
| 18 April | Type Inference | notes | P 22 | HW 5 out |
| 20 April | Polymorphic λ-calculus | notes handout | P 23 | |
| 22 April | Subtype Polymorphism | notes | P 15 | |
| 25 April | Recursive Types | notes | P 20 | |
| 27 April | Equirecursive Equality | notes | P 21 | |
| 29 April | Existential Types | notes | P 24 | HW 5 due |
| 2 May | CCS | notes | HW 6 out | |
| 4 May | CCS cont'd | notes | ||
| 6 May | π-calculus | notes | Foundational Calculi | |
| 9 May | Domain-Specific Languages | NetKAT | ||
| 11 May | Probabilistic Semantics | ProbNetKAT | HW 6 due | |
| 21 May | Final Exam | |||
