NOTE: The current schedule is tentative and subject to change. Nonetheless it gives an idea of the material to be covered in this course. The lecture notes are seeded from previous years, and will be updated immediately before and after each lecture.
Key to readings: P = Pierce; SF = Software Foundations; M = Mitchell; W = Winskel; K = Krishnamurthi 1st ed.; K2nd = Krishnamurthi 2nd ed.; 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 Stephen Chong, Nada Amin, Radu Rugina, Andrew Myers, Nate Foster, Jeff Vaughan, and Christos Dimoulas.
Videos of the lecture and section are available on Canvas.
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 | Slides | Code | Assignments | Semantics |
|---|---|---|---|---|---|---|---|
| 1 | Tue 24-Jan | Intro to semantics | P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2 | Assignment 0 due Wed Jan 25 | |||
| 2 | Thu 26-Jan | Small-step semantics | |||||
| 3 | Tue 31-Jan | Induction | A1 released | ||||
| 4 | Thu 2-Feb | Large-step semantics | |||||
| 5 | Tue 7-Feb | IMP: a simple imperative language | |||||
| 6 | Thu 9-Feb | Denotational semantics | Lambda calculus | ||||
| 7 | Tue 14-Feb | Lambda calculus | P 5 M 4.2 K 22 | A1 due; A2 released | |||
| 8 | Thu 16-Feb | Lambda calculus encodings and Recursion | |||||
| 9 | Tue 21-Feb | Definitional translations | |||||
| 10 | Thu 23-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Types | |||
| 11 | Tue 28-Feb | Simply-typed lambda calculus Type soundness |
P 9 SF2-Stlc M 6.1, 6.2 K 24-26 | A2 due | |||
| 12 | Thu 2-Mar | MID-TERM EXAM (Covers lectures 1-10) | A3 released | ||||
| 13 | Tue 7-Mar | More types | P 11, 13 SF2-Stlc2 | ||||
| 14 | Thu 9-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | Spring Recess | |||
| 15 | Tue 21-Mar | Curry-Howard isomorphism; Existential types | P 9.4 SF1-ProofObjects | A4 released | |||
| 16 | Thu 23-Mar | Type inference | P 22 K 30 | A3 due | |||
| 17 | Tue 28-Mar | Sub-structural type systems | |||||
| 18 | Thu 30-Mar | Algebraic structures | Reasoning About Programs | ||||
| 19 | Tue 4-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare | A5 released | |||
| 20 | Thu 6-Apr | Dependent types | A4 due | Misc. Topics | |||
| 21 | Tue 11-Apr | Logic Programming | M 15 K32-34 | ||||
| 22 | Thu 13-Apr | Embedded EthiCS (Guest lecturer: Michael Pope) | A6 released | ||||
| 23 | Tue 18-Apr | Dynamic Types | |||||
| 24 | Thu 20-Apr | Guest lecture: Prof. Nada Amin | A5 due | ||||
| 25 | Tue 25-Apr | Issues in language design | |||||
| Thu 27-Apr | A6 due | ||||||
| Fri 5-May | FINAL EXAM: 2pm-5pm, Science Center E |