NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course.
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 by Radu Rugina, Andrew Myers, Nate Foster, and Jeff Vaughan.
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 29-Jan | Intro to semantics | W 2,3,4 P 2.4, 3 H 2 | ||
| 2 | Thu 31-Jan | Small-step semantics | |||
| 3 | Tue 5-Feb | Induction | |||
| 4 | Thu 7-Feb | Large-step semantics | Assignment 1 released | ||
| 5 | Tue 12-Feb | IMP: a simple imperative language | |||
| 6 | Thu 14-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |
| 7 | Tue 19-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||
| 8 | Thu 21-Feb | Lambda calculus encodings and Recursion | Assignment 1 due Assignment 2 released |
||
| 9 | Tue 26-Feb | Definitional translations | |||
| 10 | Thu 28-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Types | |
| 11 | Tue 5-Mar | Simply-typed lambda calculus Type soundness |
P 9 M 6.1, 6.2 K 24-26 | ||
| 12 | Thu 7-Mar | More types | P 11, 13 | Assignment 2 due | |
| 13 | Tue 12-Mar | MID-TERM EXAM (Covers lectures 1-10) |
Assignment 3 released | ||
| 14 | Thu 14-Mar | Type inference | P 22 K 30 | Spring Recess | |
| 15 | Tue 26-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | ||
| 16 | Thu 28-Mar | Curry-Howard isomorphism; Existential types | P 9.4 | Assignment 3 due Assignment 4 released |
|
| 17 | Tue 2-Apr | Sub-structural type systems | |||
| 18 | Thu 4-Apr | Algebraic structures | Reasoning About Programs | ||
| 19 | Tue 9-Apr | Axiomatic Semantics and Hoare Logic | |||
| 20 | Thu 11-Apr | Dependent types | Assignment 4 due Assignment 5 released |
||
| 21 | Tue 16-Apr | Proof tools | |||
| 22 | Thu 18-Apr | Specification of ethical concerns (Embedded EthiCS module) Guest Lecturer: Diana Acosta Navas In-person lecture attendance expected |
Misc. Topics | ||
| 23 | Tue 23-Apr | Logic Programming | M 15 K32-34 | ||
| 24 | Thu 25-Apr | Specification of ethical concerns (Embedded EthiCS module) Guest Lecturer: Diana Acosta Navas In-person lecture attendance expected |
Assignment 5 due Assignment 6 released |
||
| 25 | Tue 30-Apr | Dynamic types | |||
| Thu 2-May | Assignment 6 due | ||||
| Thu 9-May | FINAL EXAM: 9am-12pm in Science Center D |