Chantal Keller (MSR Cambridge - INRIA)

F*: Higher-Order Effectful Program Verification

F* is an ML-like language designed for program verification. It is based on refinement types, a powerful extension of ML types to express properties about programs. These properties are automatically checked via the generation of verification conditions that are finally discharged by SMT solvers. F* provides a uniform framework to deal both with programs with effects and non-termination, for which one might want to establish some properties, and pure and terminating programs, that can also be used inside the logical refinements. To this end, it relies on a fine-grained control of effects and a termination checker based on a semantic criterion. F* finally generates code to various backends, ranging from OCaml to JavaScript.

After giving an overview of this language, I will present some aspects of its internals, in particular the treatment of effects and termination, and the generation of verification conditions all the way down to SMT solvers. I will finally discuss ongoing work on a full certification of F*.