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.

AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI   Info

Public Audience

English

60 Minutes

Saarbrücken

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.

Sabine Nermerich

302-3585

--email hidden

passcode not visible

logged in users only