(... to be written)
Source
Roman Plášil showed in 2016 how to use F* in his talk "Introduction to F* Verified Programming", tracking the official F* tutorial:
Cătălin Hriţcu gave 2018 a talk on F*: "Verified Effectful Programming in F*" (slides).
Guido Martinez talk 2017 about "F*: Tactics, SMT, and metaprogramming":
The F* language home page is at [FStar]. It contains background information. F* itself can be downloaded via Github[FstarGitHub]. A lot more information about F* are on the F* Wiki[FStarWiki]. To get started, there' a nice interactive F* tutorial for those who are already familiar with OCaml[OCaml] or any other ML variant.
Literature
- [S16] Nikhil Swamy, et al.: Dependent Types and Multi-monadic Effects in F*. In: POPL 2016. (full pdf) (slides)
- [H18] Cătălin Hriţcu: The Formal Semantics and Evolution of the F* Verification System (full pdf)
- [FStar] F*: A Higher-Order Effectful Language Designed for Program Verification
- [FStarWiki] The F* Wiki
- [FStarGitHub] F* on GitHub
- [OCaml] The OCaml System
