Schedule
| # | Topic | Dates | Materials | Comments |
|---|---|---|---|---|
| 1 | First day of class | 16/01 | slides (pdf, key) | Benjamin Pierce, “Lambda the Ultimate TA”, Terence Tao, “AI and Mathematics”, Terence Tao, “Machine assisted Proofs” |
| 2 | Functional Programming | 17/01, 20/01 | Coq | |
| 3 | Logic | 20/01, 22/01, 23/01 | Coq | |
| 4 | Induction | 23/01, 24/01, 27/01 | Coq | |
| 5 | BasicSyntax | 29/01, 30/01, 31/01 | Coq | |
| 6 | Interpreters | 31/01, 03/02, 06/02 | Coq, slides (key), slides (pdf) | |
| 7 | Logic Programming | 07/02, 12/02 | Coq | c.f. CS3100 Prolog parts |
| 8 | Functional Programming in F* | 13/02, 14/02, 17/02 | slides(key), slides(pdf), fst | See F* book mentioned in resources |
| 9 | Verifying Functional Programs in F* | 17/02, 19/02, 21/02, 24/02 | verification, quicksort, [Lowstar](quicksort | |
| 10 | Transition Systems | 24/02, 27/02, 03/03, 05/03 | Coq, slides (key), slides (pdf) | |
| 11 | Operational Semantics | 05/03, 06/03, 07/03, 10/03, 12/03, 13/03 | Coq, slides (key), slides (pdf) | |
| 12 | Lambda Calculus | 13/03, 17/03, 19/03 | Coq, slides (key), slides (pdf) | |
| 13 | Evaluation Contexts | 20/03, 21/03, 24/03 | Coq, slides (key), slides (pdf) | |
| 13 | Hoare Logic | 24/03, 26/03 | Coq, slides (key), slides (pdf) | |
| 14 | Effectful Programming in F* | fst | ||
| 15 | Pulse – concurrent separation logic |