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, Jeff Vaughan, and Christos Dimoulas.
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 27-Jan | Intro to semantics, Proof tools | P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2 | Dafny
Lean OCaml Rocq |
|||
| 2 | Thu 29-Jan | Small-step semantics | Rocq | ||||
| 3 | Tue 3-Feb | Induction | Rocq | Assignment 1 released | |||
| 4 | Thu 5-Feb | Large-step semantics | Rocq | ||||
| 5 | Tue 10-Feb | IMP: a simple imperative language | Rocq | ||||
| 6 | Thu 12-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |||
| 7 | Tue 17-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||||
| 8 | Thu 19-Feb | Lambda calculus encodings and Recursion | livecode | ||||
| 9 | Tue 24-Feb | Definitional translations | OCaml
Racket |
Assignment 1 due Assignment 2 released |
|||
| 10 | Thu 26-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | OCaml
Racket Scheme |
Types | ||
| 11 | Tue 3-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 5-Mar | More types | P 11, 13 SF2-MoreStlc SF2-References | OCaml | Assignment 2 due | ||
| 12 | Tue 10-Mar | MIDTERM IN CLASS |
Assignment 3 released | ||||
| 14 | Thu 12-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | No Class (Spring Recess) | |||
| 15 | Tue 24-Mar | Curry-Howard correspondence; Existential types | P 9.4, 24 SF1-ProofObjects Wadler'15 Ariola'24 | Haskell | |||
| 16 | Thu 26-Mar | Type Inference | P 22 K30 | Prolog | |||
| 17 | Tue 31-Mar | Sub-structural type systems | eg1.rs eg2.rs eg3.rs eg4.rs eg5.rs |
Assignment 3 due Assignment 4 released |
|||
| 18 | Thu 2-Apr | Algebraic structures | lecture.hs m.hs agediff.hs io.hs state.hs lst.hs walk.hs |
Reasoning About Programs | |||
| 19 | Tue 7-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare W 6 (W 7) | hoare.c hoare.dfy factorial.c factorial.dfy factorial2.dfy sum.dfy |
|||
| 21 | Thu 9-Apr | Logic Programming Guest Lecture: Will Byrd |
M 15 K32-34 | Notebook livecode |
|||
| 20 | Tue 14-Apr | Dependent types | Twelf
Rocq |
Assignment 4 due Assignment 5 released |
Misc. Topics | ||
| 22 | Thu 16-Apr | Embedded Ethics: Michael Pope | |||||
| 24 | Tue 21-Apr | Concurrency | M 14 A Tour of Go: Concurrency | ex1.go ex2.go ex3.go |
Assignment 6 released | ||
| 25 | Thu 23-Apr | Guest Lecture: Stephen Chong | Assignment 5 due | ||||
| 23 | Tue 28-Apr | Lecture on Research | Assignment 6 due | ||||
| TBD TBD-May | FINAL EXAM |