T9: A Tutorial on Verifying Higher-Order, Effectful Programs Using F*

  • Nikhil Swamy Microsoft Research / INRIA Paris
  • Catalin Hritcu Microsoft Research / INRIA Paris
September 04, 2015 9:00 AM - 12:30 PM

Abstract

F* is a new ML-like programming language for verifying higher-order, effectful programs. Specifications are expressed using refinement types and pre- and post-conditions on computations, and the produced verification conditions are discharged using an SMT solver. F* has been successfully used to verify a variety of programs, including the security of cryptographic protocol implementations; authorization properties of web browser extensions and cloud-hosted web applications; memory invariants of a model of the JavaScript runtime; and even the soundness of the F* type-checker itself. The latest version of F* is programmed in F*, bootstraps in both OCaml and F# on all major platforms, and is open source.

Tutorial objectives

This half-day tutorial will begin with a short introductory lecture on F*. The rest of the time will be spent working in smaller groups in interactive mode, using the F* tool to program and verify the correctness of a number of small programs, including purely functional and effectful programs, and some small security-oriented examples. Depending on interest, we will also cover the use of F* as a proof assistant, showing how it can be used to mechanize the metatheory of the simply-typed lambda calculus.

Infrastructure: We will use the online tutorial and web editor for F*, so participants do not need to install anything on their machines, but they need a working internet connection. As a fallback, F* binaries for various platforms and source code are available at GitHub and can be downloaded and installed in advance.

Target audience

Functional programmers with an interest (but not necessarily experience) in formal verification.

F*

F*

F* is a collaborative effort between Microsoft Research, INRIA, and IMDEA Software Institute. This tutorial will be delivered by Nikhil Swamy, Catalin Hritcu. The F* team also includes Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Simon Forest, Cédric Fournet, Chantal Keller, Aseem Rastogi, Pierre-Yves Strub