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 sporadically updated.
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 sections are available on Canvas. The same site also provides a Zoom link for live streaming of and remote participation in lectures.
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 26-Jan | Intro to semantics, Proof tools | P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2 | OCaml
Coq |
|||
| 2 | Thu 28-Jan | Small-step semantics | Coq | ||||
| 3 | Tue 2-Feb | Induction | Coq | Assignment 1 released | |||
| 4 | Thu 4-Feb | Large-step semantics | Coq | ||||
| 5 | Tue 9-Feb | IMP: a simple imperative language | Coq | ||||
| 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 | ||||
| 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 | Assignment 1 due Assignment 2 released |
Types | ||
| 11 | Tue 2-Mar | Simply-typed lambda calculus Type soundness |
P 9 SF2-Stlc SF2-StlcProp M 6.1, 6.2 K 24-26 (P 12) | ||||
| 13 | Thu 4-Mar | More types | P 11, 13 SF2-MoreStlc SF2-References | ||||
| 12 | Tue 9-Mar | NO CLASS MIDTERM |
|||||
| 14 | Thu 11-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | Assignment 3 released | No Class | ||
| 15 | Thu 18-Mar | Curry-Howard isomorphism; Existential types | P 9.4 SF1-ProofObjects | Haskell | Assignment 2 due | ||
| 16 | Tue 23-Mar | Type Inference | P 22 K30 | Prolog | |||
| 17 | Thu 25-Mar | Sub-structural type systems | eg1.rs eg2.rs eg3.rs eg4.rs eg5.rs |
Assignment 3 due Assignment 4 released |
|||
| 18 | Tue 30-Mar | Algebraic structures | m.hs agediff.hs io.hs state.hs |
Reasoning About Programs | |||
| 19 | Thu 1-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare W 6 (W 7) | hoare.c hoare.dfy factorial.c factorial.dfy |
|||
| 20 | Tue 6-Apr | Dependent types | Twelf | ||||
| 0 | Thu 8-Apr | Embedded EthiCS: Specifications of Ethical Concerns | Assignment 4 due Assignment 5 released |
Misc. Topics | |||
| 21 | Tue 13-Apr | Logic Programming (Guest appearance: Will Byrd) |
M 15 K32-34 | No Class | |||
| 22 | Tue 20-Apr | Probabilistic Programming (Guest lecturer: Yizhou Zhang) |
|||||
| 25 | Thu 22-Apr | Semantics for Verified Software-Hardware Stacks (Guest lecturer: Samuel Gruetter) |
Assignment 5 due Assignment 6 released |
||||
| 24 | Tue 27-Apr | Concurrency | M 14 | ex1.go ex2.go ex3.go |
|||
| Thu 29-Apr | Assignment 6 due | ||||||
| TBD TBD-May | FINAL EXAM: TBD |