Program Verification with F*
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 on
http://fpchat.com/