Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:F*: A tool for programming and proving
Speaker:Nikhil Swamy
coming from:RiSE group at MSR Redmond
Speakers Bio: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.

Event Type:CISPA Distinguished Lecture Series
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:Public Audience
Date, Time and Location
Date:Thursday, 28 April 2016
Duration:60 Minutes
Building:E9 1 - CISPA
Room: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

See for more information.
Name(s):Sabine Nermerich
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:NoTo Location:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Created by:Sabine Nermerich/AG4/MPII/DE, 03/15/2016 03:42 PMLast modified by:Uwe Brahm/MPII/DE, 04/28/2016 07:01 AM
  • Sabine Nermerich, 03/15/2016 03:49 PM -- Created document.