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

• Online editor
• Other ways to install F*

More references

• F* website
• F* tutorial
• F* code on GitHub
• #fstar Slack channel onhttp://fpchat.com/