Lectures

1. First Day of Class
   • 0_first_day_of_class.key
2. Functional Programming in Coq
   • FunctionalProgramming.v
   • FunctionalProgramming.html
3. Logic
   • Logic.v
   • Logic.html
4. Induction Principles
   • Induction.v
   • Induction.html
5. Basic Syntax
   • BasicSyntax.v
6. Interpreters
   • Interpreters.v
7. Logic Programming
   • LogicProgramming.v
8. Transition Systems
   • TransitionSystems.v
9. OperationalSemantics
   • OperationalSemantics.v
10. Lambda Calculus
    • LambdaCalculus.v
11. Hoare Logic
    • HoareLogic.v
12. Functional Programming in F*
    • fstar_functional.fst
    • 1_fstar_functional_programming.key
13. Verifying Functional Programs in F*
    • fstar_verification.fst