| layout | title | permalink |
|---|---|---|
page |
Schedule |
/schedule/ |
| # | Topic | Dates | Materials | Comments |
|---|---|---|---|---|
| 1 | First day of class | 01/02 | slides (key), slides (pdf) | Lambda, the Ultimate TA |
| 2 | Functional Programming in Coq | 02/02, 03/02 | Coq, notes | |
| 3 | Logic | 03/02, 04/02, 08/02 | Coq, notes | Proposition as Types |
| 4 | Induction | 09/02, 10/02, 11/02 | Coq, notes | |
| 5 | BasicSyntax | 11/02, 15/02, 16/02 | Coq | |
| 6 | Interpreters | 16/02, 17/02, 18/02, 01/03 | Coq, slides (key), slides (pdf) | |
| 7 | Functional Programming in F* | 01/03, 02/03, 03/03 | slides(key), slides(pdf), fst | Nik Swamy's OPLSS lectures |
| 8 | Verifying Functional Programs in F* | 04/03, 06/03 (2 * 50 minutes) | fst | |
| 9 | Logic Programming | 08/03, 09/03, 10/03 | Coq | |
| 10 | Transition Systems | 10/03, 11/03, 15/03 | Coq, slides (key), slides (pdf) | |
| 11 | Operational Semantics | 16/03, 17/03, 18/03, 22/03, 23/03 | Coq, slides (key), slides (pdf) | |
| 12 | Lambda Calculus | 24/03, 25/03, 05/04, 12/04 | Coq, slides (key), slides (pdf) | |
| 13 | Compiler Correctness | 15/04, 19/04, 20/04, 21/04, 22/03 | Coq, slides (key), slides (pdf) | |
| 14 | Hoare Logic | 22/03, 26/03, 27/03, 28/03 | Coq, Scribbles, slides (key), slides (pdf) | Software Foundations: Vol 2 Programming Language Foundations: Hoare Logic, parts I and II |
| 15 | Programming with Effects in F* | fst |