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. 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 26-Jan | Intro to semantics | W 2,3,4 P 2.4, 3 H 2 | ||
| 2 | Thu 28-Jan | Small-step semantics Inductive definitions |
Assignment 0 released | ||
| 3 | Tue 2-Feb | Inductive proofs; Large-step semantics | |||
| 4 | Thu 4-Feb | Large-step semantics, ctd. | Assignment 1 released | ||
| 5 | Tue 9-Feb | IMP: a simple imperative language | |||
| 6 | Thu 11-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |
| 7 | Tue 16-Feb | Lambda calculus | P 5 M 4.2 K 22 | Assignment 1 due Assignment 2 released |
|
| 8 | Thu 18-Feb | Lambda calculus encodings and Recursion | |||
| 9 | Tue 23-Feb | Definitional translations | |||
| 10 | Thu 25-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Types | |
| 11 | Tue 1-Mar | Simply-typed lambda calculus Type soundness |
P 9 M 6.1, 6.2 K 24-26 | Assignment 2 due Assignment 3 released |
|
| 12 | Thu 3-Mar | MID-TERM EXAM (Covers lectures 1-10) |
|||
| 13 | Tue 8-Mar | More types | P 11, 13 | ||
| 14 | Thu 10-Mar | Type inference | P 22 K 30 | Spring Recess | |
| 15 | Tue 22-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | Assignment 3 due Assignment 4 released |
|
| 16 | Thu 24-Mar | Curry-Howard isomorphism; Existential types | P 9.4 | ||
| 17 | Tue 29-Mar | Sub-structural type systems | |||
| 18 | Thu 31-Mar | Algebraic structures | Logic Programming | ||
| 19 | Tue 5-Apr | Logic Programming | M 15 K32-34 | Assignment 4 due Assignment 5 released |
Concurrency |
| 20 | Thu 7-Apr | Semantics of concurrency | M 14 | ||
| 21 | Tue 12-Apr | Language abstractions for concurrency | Contracts and control | ||
| 22 | Thu 14-Apr | Dynamic types | |||
| 23 | Tue 19-Apr | Lambda calculus machines | Assignment 5 due Assignment 6 released |
||
| 24 | Thu 21-Apr | Control-flow analysis | Tail call | ||
| 25 | Tue 26-Apr | Issues in language design | Assignment 6 due | ||
| Thu 5-May | FINAL EXAM, 9am |