Program Verification with F* (original) (raw)
Part of MPRI 2-30 course, Paris, January 2017
Lecturers: Cătălin Hriţcu and Jonathan Protzenko
Materials
- Week 1: A Gentle Introduction to F* (Code from the slides,Exercises)
- Week 2: Program Verification with F* (Code)
- Week 3: Low-level and stateful programming using F* (Exercises)
- Week 4: From "Hoare Logic" to "Dijkstra Monads" (Org file)
- Recap week: AbstractStack.fst;AbstractStackClient.fst;StatefulStack.fst;BinaryTrees.fst
Setup
More references
- F* website
- F* tutorial
- F* code on GitHub
- #fstar Slack channel onhttp://fpchat.com/