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 23-Jan | Intro to semantics, Proof tools | P 2.4, 3 SF1-Induction,Imp SF2-SmallStep W 2,3,4 H 2 | Dafny
OCaml Coq |
|||
| 2 | Thu 25-Jan | Small-step semantics | Coq | ||||
| 3 | Tue 30-Jan | Induction | Coq | Assignment 1 released | |||
| 4 | Thu 1-Feb | Large-step semantics | Coq | ||||
| 5 | Tue 6-Feb | IMP: a simple imperative language | Coq | ||||
| 6 | Thu 8-Feb | Denotational semantics (Kevin Zhang) |
W 5 M 4.3 | Lambda calculus | |||
| 7 | Tue 13-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||||
| 8 | Thu 15-Feb | Lambda calculus encodings and Recursion | livecode | ||||
| 9 | Tue 20-Feb | Definitional translations | OCaml
Racket |
Assignment 1 due Assignment 2 released |
|||
| 10 | Thu 22-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | OCaml
Racket |
Types | ||
| 11 | Tue 27-Feb | Simply-typed lambda calculus Type soundness |
P 9 SF2-Stlc SF2-StlcProp M 6.1, 6.2 K 24-26 (P 12) | ||||
| 13 | Thu 29-Feb | More types | P 11, 13 SF2-MoreStlc SF2-References | OCaml | Assignment 2 due | ||
| 12 | Tue 5-Mar | NO CLASS MIDTERM |
Assignment 3 released | ||||
| 14 | Thu 7-Mar | Parameteric Polymorphism, Records and Subtyping (Anastasiya Kravchuk-Kirilyuk) |
P 23 M 6.4 P 11.8, 15 | No Class (Spring Recess) | |||
| 15 | Tue 19-Mar | Curry-Howard correspondence; Existential types (Zena Ariola) |
P 9.4, 24 SF1-ProofObjects | Haskell | |||
| 16 | Thu 21-Mar | Type Inference | P 22 K30 | Prolog | |||
| 17 | Tue 26-Mar | Sub-structural type systems (Cameron Wong) |
eg1.rs eg2.rs eg3.rs eg4.rs eg5.rs |
Assignment 3 due Assignment 4 released |
|||
| 18 | Thu 28-Mar | Algebraic structures (Raffi Sanna) |
lecture.hs m.hs agediff.hs io.hs state.hs lst.hs walk.hs |
Reasoning About Programs | |||
| 19 | Tue 2-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare W 6 (W 7) | hoare.c hoare.dfy factorial.c factorial.dfy factorial2.dfy sum.dfy |
|||
| 20 | Thu 4-Apr | Dependent types | Twelf
Coq |
Misc. Topics | |||
| 22 | Tue 9-Apr | Embedded EthiCS (Anni Raety) |
Assignment 4 due Assignment 5 released |
||||
| 21 | Thu 11-Apr | Logic Programming (Will Byrd) |
M 15 K32-34 | Notebook livecode |
|||
| 24 | Tue 16-Apr | Concurrency | M 14 | ex1.go ex2.go ex3.go |
Assignment 6 released | ||
| 25 | Thu 18-Apr | Guest Lecture on Making OCaml Safe for Performance Engineering by Ron Minsky | Assignment 5 due | ||||
| 23 | Tue 23-Apr | Guest Lecture on Rust by Niko Matsakis | Assignment 6 due | ||||
| Mon 6-May | FINAL EXAM: May 6 |