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, Radu Rugina, Andrew Myers, Nate Foster, and Jeff Vaughan.
Videos of the lecture and section are available on Canvas / Extension Class Meetings. 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 | Slides | Code | Assignments | Semantics |
|---|---|---|---|---|---|---|---|
| 0 | Tue 28-Jan | Intro to semantics, Proof tools | P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2 | ||||
| 1 | Thu 30-Jan | Intro to semantics, Proof tools | |||||
| 2 | Tue 4-Feb | Small-step semantics | Coq
|
Assignment 1 released | |||
| 3 | Thu 6-Feb | Induction | Coq
|
||||
| 4 | Tue 11-Feb | Large-step semantics | |||||
| 5 | Thu 13-Feb | IMP: a simple imperative language | |||||
| 6 | Tue 18-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |||
| 7 | Thu 20-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||||
| 8 | Tue 25-Feb | Lambda calculus encodings and Recursion | |||||
| 9 | Thu 27-Feb | Definitional translations | Assignment 1 due Assignment 2 released |
||||
| 10 | Tue 3-Mar | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | Types | |||
| 11 | Thu 5-Mar | Simply-typed lambda calculus Type soundness |
P 9 SF2-Stlc M 6.1, 6.2 K 24-26 | ||||
| 12 | Tue 10-Mar | NO CLASS (Take midterm on Canvas by 24-Mar) |
|||||
| 13 | Thu 12-Mar | More types | P 11, 13 SF2-Stlc2 | Assignment 3 released | 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 SF1-ProofObjects | Assignment 2 due | |||
| 16 | Tue 31-Mar | Type inference | P 22 K 30 | Assignment 4 released | |||
| 17 | Thu 2-Apr | Sub-structural type systems | Assignment 3 due | ||||
| 18 | Tue 7-Apr | Algebraic structures | Reasoning About Programs | ||||
| 19 | Thu 9-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare | ||||
| 20 | Tue 14-Apr | Dependent types | Assignment 4 due; Assignment 5 released | Misc. Topics | |||
| 21 | Thu 16-Apr | Logic Programming | M 15 K32-34 | ||||
| 22 | Tue 21-Apr | Probabilistic Programming | Guest lecturer: Yizhou Zhang | ||||
| 23 | Thu 23-Apr | Dynamic Types | .rkt
|
||||
| 24 | Tue 28-Apr | Semantics of Concurrency | |||||
| Fri 1-May | Assignment 5 due | ||||||
| TBD TBD-May | FINAL EXAM: TBD |