| 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 |
|