# Schedule

# | Topic | Dates | Materials | Comments |
---|---|---|---|---|

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 | Coq, notes | Proposition as Types | |

4 | Induction | Coq, notes | ||

5 | BasicSyntax | Coq | ||

6 | Interpreters | Coq | ||

7 | Logic Programming | Coq | ||

8 | Transition Systems | Coq | ||

9 | Operational Semantics | Coq | ||

10 | Lambda Calculus | Coq | ||

11 | Hoare Logic | Coq | ||

12 | Functional Programming in F* | slides(pdf), fst | ||

12 | Verifying Functional Programs in F* | fst |