RiSE group at MSR Redmond
Title : F*: A tool for programming and proving
Building: E9 1 (CISPA), Room 0.05, Lecture hall
Proving and programming are inextricably linked, especially in dependent type theory, where constructive proofs are just programs. However, not all programs are proofs. Effective programmers
routinely go beyond a language of pure, total functions and use features like non-termination, state, exceptions, and IO—features that one does not usually expect in proofs.
F* is a new language from Microsoft Research and INRIA that aims to provide equal facilities for general purpose programming (as in languages like OCaml and Haskell) and for proving (as in proof assistants like Coq or Agda), while providing automation for proofs via SMT solvers (like Boogie or Why3).
In this talk, I present a broad overview of the design of F*, while touching upon some new features of the language, notably, reasoning about effectful programs via monadic reflection.
Traditionally, the main applications of F* have been in verifying implementations of cryptographic protocols. I will describe our recent efforts at verifying an implementation of TLS-1.3, as well as some new application areas for F*, including side-channel resistant implementations of elliptic curves and the verification of quantum compilers.
See https://fstar-lang.org for more information.
I am a Researcher in the RiSE group at MSR Redmond and the main designer and implementer of F*. My work covers various topics including type systems, program logics, functional programming,
program verification and interactive theorem proving. I often think about how to use these techniques to build provably secure programs, including web applications, web browsers, crypto protocol
implementations, and low-level systems code.