# Topic Dates Lec Hours Materials Comments
1 First day of class 16/01 1 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 1.5 Coq  
3 Logic 20/01, 22/01, 23/01 2 Coq  
4 Induction 23/01, 24/01, 27/01 2.5 Coq  
5 BasicSyntax 29/01, 30/01, 31/01 2.5 Coq  
6 Interpreters 31/01, 03/02, 06/02 2.5 Coq, slides (key), slides (pdf)  
7 Logic Programming 07/02, 12/02 2 Coq c.f. CS3100 Prolog parts
8 Functional Programming in F* 13/02, 14/02, 17/02 2.5 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 3 verification, quicksort, [Lowstar](quicksort  
10 Transition Systems 24/02, 27/02, 03/03, 05/03 3 Coq, slides (key), slides (pdf)  
11 Operational Semantics 05/03, 06/03, 07/03, 10/03, 12/03, 13/03 5 Coq, slides (key), slides (pdf)  
12 Lambda Calculus 13/03, 17/03, 19/03 2.5 Coq, slides (key), slides (pdf)  
13 Evaluation Contexts 20/03, 21/03, 24/03 2.5 Coq, slides (key), slides (pdf)  
13 Hoare Logic 24/03, 26/03, 27/03, 02/04 3 Coq, slides (key), slides (pdf)  
14 Effectful Programming in F* 02/04, 03/04, 04/04 2 fst  
15 Pulse – concurrent separation logic 04/04, 07/04, 09/04, 11/04, 16/04, 17/04, 21/04, 23/04 7.5 fst book


Total lecture hours = 45.