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 |
|---|---|---|---|---|---|
| Tue 26-Jan | Class canceled due to weather | ||||
| 1 | Thu 28-Jan | Intro to semantics Small-step semantics |
W 2,3,4 P 2.4, 3 H 2 | Assignment 0 released | |
| 2 | Tue 3-Feb | Inductive definitions and proof | |||
| 3 | Thu 5-Feb | Large-step semantics | Assignment 1 released | ||
| Tue 10-Feb | Class canceled due to weather | ||||
| 4 | Thu 12-Feb | IMP: a simple imperative language | Assignment 1 due Assignment 2 released |
||
| 5 | Fri 13-Feb | Denotational semantics Available on video only; video is from last year: ignore time-based information. See above for link to videos. |
W 5 M 4.3 | Lambda calculus | |
| 6 | Tue 17-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||
| 7 | Thu 19-Feb | Lambda calculus encodings and Recursion | Assignment 2 due Assignment 3 released |
||
| 8 | Tue 24-Feb | Definitional translations | |||
| 9 | Thu 26-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Assignment 3 due Assignment 4 released |
|
| 10 | Tue 3-Mar | MID-TERM EXAM | Types | ||
| 11 | Thu 5-Mar | Simply-typed lambda calculus Type soundness |
P 9 M 6.1, 6.2 K 24-26 | ||
| 12 | Tue 10-Mar | More types | P 11, 13 | Assignment 4 due Assignment 5 released |
|
| 13 | Thu 12-Mar | Type inference | P 22 | Spring Recess | |
| 14 | Tue 24-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | ||
| 15 | Thu 26-Mar | Curry-Howard isomorphism; Existential types | P 9.4 | Assignment 5 due Assignment 6 released |
|
| 16 | Tue 31-Mar | Algebraic structures | Concurrency | ||
| 17 | Thu 2-Apr | Semantics of concurrency | Assignment 6 due Assignment 7 released |
||
| 18 | Tue 7-Apr | Language abstractions for concurrency | Contracts and control | ||
| 19 | Thu 9-Apr | Dynamic types | PDF Guest lecturer: Christos Dimoulas |
Assignment 7 due Assignment 8 released |
|
| 20 | Tue 14-Apr | Lambda calculus machines | PDF Guest lecturer: Christos Dimoulas |
||
| 21 | Thu 16-Apr | Delimited control | PDF Guest lecturer: Christos Dimoulas |
||
| 22 | Tue 21-Apr | Control-flow analysis | Assignment 8 due | Miscellany | |
| 23 | Thu 23-Apr | Logic programming | Assignment 9 released | ||
| 24 | Tue 28-Apr | Functional Reactive Programming | |||
| 25 | Thu 30-Apr | Reading period make-up lecture due to canceled classes Common mistakes in programming language design |
Assignment 9 due |