| 1 |
First day of class |
13/01 |
slides (key), slides (pdf) |
Lambda, the Ultimate TA |
| 2 |
Functional Programming in Coq |
14/01, 16/01 |
Coq, notes |
|
| 3 |
Logic |
16/01, 20/01, 21/01, 22/01 |
Coq, notes |
Proposition as Types |
| 4 |
Induction |
23/01, 27/01, 28/01 |
Coq, notes |
|
| 5 |
BasicSyntax |
29/01, 30/01 |
Coq |
|
| 6 |
Interpreters |
03/02, 04,02, 05/02 |
Coq |
|
| 7 |
Logic Programming |
05/02, 06/02 |
Coq |
|
| 8 |
Transition Systems |
10/2 + tutorial, 11/2, 12/2, 13/2, 17/2 + tutorial, 18/2 |
Coq, slides (key), slides (pdf) |
|
| 9 |
Operational Semantics |
19/2, 20/2, 24/2 (only tutorial), 25/2 (only tutorial), 26/2, 27/2, 02/03 (only tutorial), 03/03, 05/03, tutorial (36 min of video released on 1/4; Pset7 opsem solutions) |
Coq, slides (key), slides (pdf) |
|
| 10 |
Lambda Calculus |
05/03, 09/03 + tutorial, 11/03, 12/03, 16/03, 66 min of videos released on 31/3, tutorial (38 min of video released on 1/4; subtyping), tutorial (31 min video on 13/04; PSet8 subtyping solution) |
Coq, slides (key), slides (pdf) |
|
| 11 |
Hoare Logic |
86 min of videos released on 06/04, 30 min of videos released on 07/04 |
Coq, Scribbles, slides (key), slides (pdf) |
Software Foundations: Vol 2 Programming Language Foundations: Hoare Logic, parts I and II |
| 12 |
Functional Programming in F* |
86 min of videos released on 13/04 |
slides(key), slides(pdf), fst |
Nik Swamy’s OPLSS lectures |
| 13 |
Verifying Functional Programs in F* |
86 min of videos released on 14/04 |
fst |
|
| 14 |
Programming with Effects in F* |
54 min of videos released on 21/04 |
fst |
|