Write a Blog >>
Wed 20 Jan 2016 16:30 - 16:55 at Grand Bay North - Track 1: Language Design Chair(s): David Walker

We present F*, a new language that works both as a proof assistant as well as a general-purpose, verification-oriented, effectful programming language.

In support of these complementary roles, F* is a dependently typed, higher-order, call-by-value language with primitive effects including state, exceptions, divergence and IO. Although primitive, programmers choose the granularity at which to specify effects by equipping each effect with a monadic, predicate transformer semantics. F* uses this to efficiently compute weakest preconditions and discharges the resulting proof obligations using a combination of SMT solving and manual proofs. Isolated from the effects, the core of F* is a language of pure functions used to write specifications and proof terms—its consistency is maintained by a semantic termination check based on a well-founded order.

We evaluate our design on more than 55,000 lines of F* we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F* is programmed (but not verified) in F*, and bootstraps in both OCaml and F#. Our experience confirms F*’s pay-as-you-go cost model: writing idiomatic ML-like code with no finer specifications imposes no user burden. As a verification-oriented language, our most significant evaluation of F* is in verifying several key modules in an implementation of the TLS-1.2 protocol standard. For the modules we considered, we are able to prove more properties, with fewer annotations using F* than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F* in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to F-omega and even micro-F*, a sizeable fragment of F* itself—these proofs make essential use of F*’s flexible combination of SMT automation and constructive proofs, enabling a tactic-free style of programming and proving at a relatively large scale.

Wed 20 Jan
Times are displayed in time zone: Guadalajara, Mexico City, Monterrey change

16:30 - 17:45: Track 1: Language DesignResearch Papers at Grand Bay North
Chair(s): David WalkerPrinceton University
16:30 - 16:55
Dependent Types and Multi-Monadic Effects in F*
Research Papers
Nikhil SwamyMicrosoft Research, Cătălin HriţcuINRIA Paris, Chantal KellerMSR-INRIA, Aseem RastogiUniversity of Maryland, College Park, Antoine Delignat-LavaudINRIA, Simon ForestENS, Karthikeyan BhargavanINRIA, Cédric FournetMicrosoft Research, Pierre-Yves StrubIMDEA Software Institute, Markulf KohlweissMicrosoft Research, Jean-Karim ZinzindohouéINRIA, Santiago Zanella-BéguelinMicrosoft Research
Pre-print Media Attached
16:55 - 17:20
Fabular: Regression Formulas as Probabilistic Programming
Research Papers
Johannes BorgströmUppsala University, Andrew D. GordonMicrosoft Research and University of Edinburgh, Long OuyangStanford University, Claudio RussoMicrosoft Research, Adam ŚcibiorUniversity of Cambridge, Marcin SzymczakUniversity of Edinburgh
Media Attached
17:20 - 17:45
Kleenex: Compiling Nondeterministic Transducers to Deterministic Streaming Transducers
Research Papers
Bjørn Bugge GrathwohlDIKU, University of Copenhagen, Fritz HengleinDIKU, Denmark, Ulrik Terp RasmussenDIKU, University of Copenhagen, Kristoffer Aalund SøholmJobindex, Denmark, Sebastian Paaske TørholmJobindex, Denmark
Media Attached