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 | verification, quicksort, [Lowstar](quicksort | |
| 10 | Transition Systems | |||
| 11 | Operational Semantics | |||
| 12 | Lambda Calculus | |||
| 13 | Hoare Logic | |||
| 14 | Effectful Programming in F* |