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 an interactive 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 programming with and reasoning about monotonically evolving state, and for extending F* with new 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* computes verification conditions using monads of predicate transformers, aka Dijkstra monads.

The course material is available at https://danelahman.github.io/teaching/eutypes2018/ .