Speaker
Cătălin Hriţcu is a researcher of the Prosecco team at Inria Paris. He is one of the developers of the F* programming language, and is leading a research effort in secure compilation funded by an ERC starting grant. This course is thought together with Antoine Delignat-Lavaud, Danel Ahman, and Victor Dumitrescu.
Abstract
F* is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, or C code. This enables verifying the functional correctness and security of realistic applications, such as a verified HTTPS stack.
This course will give an introduction to program verification in F* using simple examples and a few, even simpler exercises along the way. We will start with specifying and verifying purely-functional programs and then move to programs with side-effects such as divergence and mutable state. We will also cover F*’s support for reasoning about monotonically evolving state and for adding extra monadic side-effects, which is for instance used to implement F*’s tactic system in F* itself. Finally, we will look a bit under the hood at how F* encodes verification conditions to the SMT and how it computes them in the first place using monads of predicate transformers, aka Dijkstra monads.