Programming Languages and Logics
MWF 9:05-9:55
Gates G01
Key: P = Pierce, W = Winskel
| Date | Topic | Notes | Reading | Assignments |
| 27 August | Course Overview | slides | ||
| 29 August | Introduction to Semantics | slides notes | W 1-2 | |
| 1 September | No class (Labor Day) | |||
| 3 September | Inductive definitions | slides notes | W 3 | HW1 out |
| 5 September | Inductive proof and Large-step Semantics | slides notes | W 2, P 3 | |
| 8 September | IMP | slides notes code | W 2 | |
| 10 September | IMP Properties | slides notes | HW1 due; HW2 out | |
| 12 September | Denotational Semantics | slides notes | W 5 | |
| 15 September | Denotational Semantics Examples | notes | ||
| 17 September | Axiomatic Semantics | slides notes | W6 | HW2 due; HW3 out |
| 19 September | Hoare Logic | slides notes | ||
| 22 September | Hoare Logic Examples | slides | ||
| 24 September | Weakest Preconditions | slides notes | W7 | HW3 due; HW4 out |
| 26 September | Lambda-calculus | notes | P5 | |
| 29 September | More Lambda-calculus and Substitution | slides notes | P5 | |
| 1 October | No class (CS 50th / Gates Dedication) | |||
| 3 October | Lambda-calculus Encodings | slides notes | ||
| 6 October | Preliminary Exam I | |||
| 8 October | Exam Debrief | |||
| 10 October | Programming in the Lambda-calculus | slides notes | ||
| 13 October | No class (Fall break) | |||
| 15 October | Definitional Translation and Continuations | slides notes | HW5 out | |
| 17 October | Simple Types | notes | ||
| 20 October | Proving Type Soundness | notes | ||
| 22 October | Normalization | slides notes | HW5 due; HW6 out | |
| 24 October | Advanced Types | slides notes | ||
| 27 October | Polymorphism | slides notes | ||
| 29 October | Type Inference | slides notes | HW 6 due; HW7 out | |
| 31 October | Compiling with Continuations | slides notes | ||
| 3 November | Records and Subtyping | slides notes | ||
| 5 November | Existential Types | slides notes | HW7 due; HW 8 out | |
| 7 November | Recursive Types | slides notes | ||
| 10 November | Propositions as Types | slides notes | ||
| 12 November | Featherweight Java | slides notes | HW 8 due | |
| 14 November | Preliminary Exam II | |||
| 17 November | Featherweight Java Properties | slides notes | ||
| 19 November | Exam Debrief | HW 9 out | ||
| 21 November | Typed Assembly Language I | slides | ||
| 24 November | Typed Assembly Language II | slides | ||
| 26 November | No class (Thanksgiving) | |||
| 28 November | No class (Thanksgiving) | |||
| 1 December | Typed Assembly Language III | slides | HW 10 out | |
| 3 December | Concurrency | slides | ||
| 5 December | Victory Lap | slides | ||