NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course. See last year's schedule for lecture notes to get a better idea.
Key to readings: M = Mitchell; W = Winskel; K = Krishnamurthi 1st ed.; K2nd = Krishnamurthi 2nd ed.; P = Pierce; H = Harper. The readings are not required, but may help your understanding of the lecture material.
The lecture notes here contain material from lecture notes of courses taught by Radu Rugina, Andrew Myers, and Nate Foster.
Videos of the lecture and section are available here. (Make sure to log in, and look on the left of the page for "Lecture Videos", etc.) The same site also provides live streams for lecture.
For background material on sets, relations, functions, and induction, see: W 1, H 2, H Appendix, and/or P 2.
| Lec. | Date | Topic | Readings | Notes | Assignments | Semantics |
|---|---|---|---|---|---|
| 1 | Tue 28-Jan | Intro to semantics Small-step semantics |
W 2,3,4 P 2.4, 3 H 2 | Assignment 0 released | |
| 2 | Thu 30-Jan | Inductive definitions and proof | |||
| 3 | Tue 4-Feb | Large-step semantics IMP: a simple imperative language |
Assignment 1 released | ||
| 4 | Thu 6-Feb | IMP | |||
| 5 | Tue 11-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |
| 6 | Thu 13-Feb | Lambda calculus | P 5 M 4.2 K 22 | Assignment 1 due Assignment 2 released |
|
| 7 | Tue 18-Feb | Lambda calculus encodings and Recursion | |||
| 8 | Thu 20-Feb | Definitional translations | |||
| 9 | Tue 25-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Assignment 2 due | Types |
| 10 | Thu 27-Feb | Simply-typed lambda calculus Type soundness |
P 9 M 6.1, 6.2 K 24-26 | ||
| 11 | Tue 4-Mar | MID-TERM EXAM | Assignment 3 released | ||
| 12 | Thu 6-Mar | More types | P 11, 13 | ||
| 13 | Tue 11-Mar | Type inference | P 22 | ||
| 14 | Thu 13-Mar | Polymorphism | P 23 M 6.4 | Spring Recess | |
| 15 | Tue 25-Mar | Records and Subtyping | P 11.8, 15 | Assignment 3 due Assignment 4 released |
|
| 16 | Thu 27-Mar | Curry-Howard isomorphism | P 9.4 | ||
| 17 | Tue 1-Apr | Existential types and modules | P 24 | ||
| 18 | Thu 3-Apr | Dynamic types | K2nd 17 | ||
| 19 | Tue 8-Apr | Algebraic structures | Assignment 4 due Assignment 5 released |
Reasoning about programs | |
| 20 | Thu 10-Apr | Axiomatic semantics and Hoare logic | W 6 | ||
| 21 | Tue 15-Apr | Abstract interpretation | |||
| 22 | Thu 17-Apr | Control-flow analysis | Assignment 5 due Assignment 6 released |
Miscellany | |
| 23 | Tue 22-Apr | Logic programming | K 33 | ||
| 24 | Thu 24-Apr | Concurrency | |||
| 25 | Tue 29-Apr | Some common mistakes in language design | |||
| Thu 1-May | Assignment 6 due |