salle A. Turing CE4
14 octobre 2015 - 14h00
F*: Higher-Order Effectful Program Verification
par Chantal Keller de Université Paris Sud
Abstract: 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
certification of F* and its use as a theorem prover.
