Dependent Types and Multi-monadic Effects in F*

<html> <header> <title>Dependent Types and Multi-monadic Effects in F*</title> </header> <body> <center> <div style="text-align: justify; width: min(90%, 50em)"> <h1 style="text-align: center"> Dependent Types and Multi-monadic Effects in F⭑ </h1> <div> <a href="artifacts"> <img src="../aec-badge-popl.png" alt="Artifact Evaluation Badge" style="float:right;width:7em;height:7em;"> </a> </div> <a href="http://research.microsoft.com/en-us/people/nswamy/">Nikhil Swamy</a>1    <a href="http://prosecco.gforge.inria.fr/personal/hritcu/">Cătălin Hriţcu</a>2    <a href="http://prosecco.gforge.inria.fr/personal/ckeller/">Chantal Keller</a>1,3    <a href="https://www.cs.umd.edu/~aseem/">Aseem Rastogi</a>4 <a href="http://antoine.delignat-lavaud.fr/">Antoine Delignat-Lavaud</a>2,5    <a href="http://www.eleves.ens.fr/home/forest">Simon Forest</a>2,5    <a href="http://prosecco.gforge.inria.fr/personal/karthik/">Karthikeyan Bhargavan</a>2    <a href="http://research.microsoft.com/en-us/um/people/fournet/">Cédric Fournet</a>1,3 <a href="http://www.strub.nu/">Pierre-Yves Strub</a>6    <a href="http://research.microsoft.com/en-us/people/markulf/">Markulf Kohlweiss</a>1    Jean-Karim Zinzindohoue2,5    Santiago Zanella-Béguelin1 1Microsoft Research    2Inria    3MSR-Inria    4UMD    5ENS Paris    6IMDEA Software Institute <a href="http://conf.researchr.org/home/POPL-2016"> Symposium on Principles of Programming Languages, POPL 2016</a> <h3>Abstract</h3> We present a new, completely redesigned, version of F⭑, a 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 System 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. <ul> <li><a href="paper.pdf">Paper (PDF)</a></li> <li><a href="artifacts">Online materials (artifact evaluated)</a></li> <li><a href="popl2016.html?transition=none">POPL 2016 slides</a></li> <li><a href="http://fstar-lang.org/">F⭑ project page</a></li> <li><a href="https://github.com/FStarLang/FStar">F⭑ on GitHub</a></li> </ul> </div> </center> </body> </html>

CINXE.COM

Dependent Types and Multi-monadic Effects in F*