Dependent types and multi-monadic effects in F

Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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ω and even μ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.
Original languageEnglish
Title of host publicationProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016
PublisherACM
Pages256-270
Number of pages15
ISBN (Electronic)978-1-4503-3549-2
DOIs
Publication statusPublished - 2016
Event43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - St. Petersburg, FL, United States
Duration: 20 Jan 201622 Jan 2016
https://popl16.sigplan.org/home

Conference

Conference43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Abbreviated titlePOPL 2016
Country/TerritoryUnited States
CitySt. Petersburg, FL
Period20/01/1622/01/16
Internet address

Fingerprint

Dive into the research topics of 'Dependent types and multi-monadic effects in F'. Together they form a unique fingerprint.

Cite this