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.
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 25-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 27-Jan | Small-step semantics | Coq | ||||
| 3 | Tue 1-Feb | Induction | Coq | Assignment 1 released | |||
| 4 | Thu 3-Feb | Large-step semantics | Coq | ||||
| 5 | Tue 8-Feb | IMP: a simple imperative language | Coq | ||||
| 6 | Thu 10-Feb | Denotational semantics | W 5 M 4.3 | Lambda calculus | |||
| 7 | Tue 15-Feb | Lambda calculus | P 5 M 4.2 K 22 | ||||
| 8 | Thu 17-Feb | Lambda calculus encodings and Recursion | livecode | ||||
| 9 | Tue 22-Feb | Definitional translations | Racket | Assignment 1 due Assignment 2 released |
|||
| 10 | Thu 24-Feb | References and continuations | P 13 M 5,4, 8.3.2 H 29, 36 K 18-20 | OCaml
Racket |
Types | ||
| 11 | Tue 1-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 3-Mar | More types | P 11, 13 SF2-MoreStlc SF2-References | OCaml | Assignment 2 due | ||
| 12 | Tue 8-Mar | NO CLASS MIDTERM |
Assignment 3 released | ||||
| 14 | Thu 10-Mar | Parameteric Polymorphism, Records and Subtyping | P 23 M 6.4 P 11.8, 15 | No Class (Spring Recess) | |||
| 15 | Tue 22-Mar | Curry-Howard correspondence; Existential types | P 9.4, 24 SF1-ProofObjects | Haskell | |||
| 16 | Thu 24-Mar | Type Inference | P 22 K30 | Prolog | |||
| 17 | Tue 29-Mar | Sub-structural type systems | eg1.rs eg2.rs eg3.rs eg4.rs eg5.rs |
Assignment 3 due Assignment 4 released |
|||
| 18 | Thu 31-Mar | Algebraic structures | m.hs agediff.hs io.hs state.hs lst.hs walk.hs |
Reasoning About Programs | |||
| 19 | Tue 5-Apr | Axiomatic Semantics and Hoare Logic | SF2-Hoare W 6 (W 7) | hoare.c hoare.dfy factorial.c factorial.dfy factorial2.dfy |
|||
| 20 | Thu 7-Apr | Dependent types | Twelf
Coq |
Misc. Topics | |||
| 22 | Tue 12-Apr | Embedded EthiCS Designing Usable Programming Languages by Eliza Wells (Guest) |
Assignment 4 due Assignment 5 released |
||||
| 21 | Thu 14-Apr | Logic Programming by Aaron Bembenek (Guest) |
M 15 K32-34 | Notebook | |||
| 23 | Tue 19-Apr | Relational Programming by William E. Byrd (Guest) |
Assignment 6 released | ||||
| 25 | Thu 21-Apr | Semantics for Verified Software-Hardware Stacks by Samuel Gruetter (Guest) |
Assignment 5 due | ||||
| 24 | Tue 26-Apr | Concurrency | M 14 | ex1.go ex2.go ex3.go |
Assignment 6 due | ||
| TBD TBD-May | FINAL EXAM: TBD |