- https://www.fstar-lang.org/
- https://fstarlang.github.io/
- https://github.com/FStarLang/FStar/wiki
- https://lists.gforge.inria.fr/pipermail/fstar-club/
- https://github.com/FStarLang/FStar
Installation
https://github.com/FStarLang/FStar/blob/master/INSTALL.md
macOS
$ brew install fstar $ fstar.exe --version # Compiling code extracted to OCaml requires Batteries etc: $ brew install opam $ opam install batteries zarith stdint # Compiling code extracted to F# requires Mono: $ brew install mono
Projects
- Project Everest, a formally verified TLS stack
Libraries
Tools
- KreMLin, a tool to extract F* programs to readable C code
Talks
- Translating from F* to C: a progress report https://jonathan.protzenko.fr/papers/talk-ml16.pdf
- Low-level and stateful programming in F* https://jonathan.protzenko.fr/mpri/20170120-protocols/pres.pdf