This half-day tutorial will begin with a short introductory lecture on F*. The rest of the time will be spent working in smaller groups in interactive mode, using the F* tool to program and verify the correctness of a number of small programs, including purely functional and effectful programs, and some small security-oriented examples. Depending on interest, we will also cover the use of F* as a proof assistant, showing how it can be used to mechanize the metatheory of the simply-typed lambda calculus.
Infrastructure: We will use the online tutorial and web editor for F*, so participants do not need to install anything on their machines, but they need a working internet connection. As a fallback, F* binaries for various platforms and source code are available at GitHub and can be downloaded and installed in advance.
Functional programmers with an interest (but not necessarily experience) in formal verification.
F* is a collaborative effort between Microsoft Research, INRIA, and IMDEA Software Institute. This tutorial will be delivered by Nikhil Swamy, Catalin Hritcu. The F* team also includes Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Simon Forest, Cédric Fournet, Chantal Keller, Aseem Rastogi, Pierre-Yves Strub