Online citations, reference lists, and bibliographies.

Dependent Types And Multi-monadic Effects In F*

N. Swamy, Catalin Hritcu, C. Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, K. Bhargavan, C. Fournet, P. Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin
Published 2016 · Computer Science

Cite This
Download PDF
Analyze on Scholarcy
Share
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.
This paper references
10.1017/S095679680900728X
Parameterised notions of computation
Robert Atkey (2009)
10.1007/978-3-642-17511-4_20
Dafny: An Automatic Program Verifier for Functional Correctness
K. Leino (2010)
10.17487/rfc8446
The Transport Layer Security (TLS) Protocol Version 1.2
T. Dierks (2008)
Towards a practical programming language based on dependent type theory
U. Norell (2007)
10.1007/978-94-011-1793-7_2
Towards a Mathematical Science of Computation
J. McCarthy (1962)
foetus - Termination Checker for Simple Functional Programs
A. Abel (2002)
10.1109/LICS.1989.39155
Computational lambda-calculus and monads
E. Moggi (1989)
10.1017/S0960129503004122
Type-based termination of recursive definitions
G. Barthe (2004)
10.1145/1375581.1375602
Liquid types
P. M. Rondon (2008)
10.1145/586110.586125
Authenticated-encryption with associated-data
P. Rogaway (2002)
Simple General Recursion in Type Theory
A. Bove (2001)
10.1145/954666.971189
Report on the programming language Euclid
B. Lampson (1977)
10.1145/1706299.1706350
Modular verification of security protocol code by typing
K. Bhargavan (2010)
10.1145/2491956.2491978
Verifying higher-order programs with the dijkstra monad
N. Swamy (2013)
10.1017/S0956796808006953
Hoare type theory, polymorphism and separation
Aleksandar Nanevski (2008)
10.1007/3-540-48168-0_32
Monadic Presentations of Lambda Terms Using Generalized Inductive Types
Thorsten Altenkirch (1999)
10.1145/1596550.1596565
Effective interactive proofs for higher-order imperative programs
Adam Chlipala (2009)
Type-based termination: a polymorphic lambda-calculus with sized higher-order types
A. Abel (2006)
10.1145/2500365.2500581
Programming and reasoning with algebraic effects and dependent types
E. Brady (2013)
Reasoning about Aliasing
M. Utting (1996)
10.1006/inco.1996.2613
Region-based Memory Management
M. Tofte (1997)
10.1007/978-3-540-69407-6_39
Extraction in Coq: An Overview
Pierre Letouzey (2008)
The Coq development team. The Coq proof assistant
10.1145/289423.289451
Cayenne—a language with dependent types
L. Augustsson (1998)
10.1007/11617990_1
Formalized Metatheory with Terms Represented by an Indexed Family of Types
R. Adams (2004)
10.1145/2500365.2500579
Mtac: a monad for typed tactic programming in Coq
Beta Ziliani (2013)
10.1145/2034773.2034811
Secure distributed programming with value-dependent types
N. Swamy (2011)
10.1007/978-3-319-22102-1_24
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
S. Schäfer (2015)
10.1145/2535838.2535883
Combining proofs and programs in a dependently typed language
Chris Casinghino (2014)
Implementing Mathematics with the Nuprl
R. L. Constable (1986)
10.1109/32.713327
Subtypes for Specifications: Predicate Subtyping in PVS
J. Rushby (1998)
Practical Foundations for Programming Languages
R. Harper (2012)
10.1007/978-3-642-37036-6_8
Why3 - Where Programs Meet Provers
J. Filliâtre (2013)
10.1145/113445.113468
Refinement types for ML
Timothy S. Freeman (1991)
10.1109/SP.2013.37
Implementing TLS with Verified Cryptographic Security
K. Bhargavan (2013)
10.1145/2541568.2541569
Refinement types for Haskell
R. Jhala (2014)
Implementing mathematics with the Nuprl proof development system
R. Constable (1986)
10.1145/360933.360975
Guarded commands, nondeterminacy and formal derivation of programs
E. Dijkstra (1975)
10.1145/2103776.2103780
Equational reasoning about programs with general recursion and call-by-value semantics
Garrin Kimmell (2012)
10.1007/978-3-540-74464-1_16
Subset Coercions in Coq
Matthieu Sozeau (2006)
Coq extraction, an overview
P Letouzey (2008)
10.1007/978-3-642-22863-6_13
Termination of Isabelle Functions via Termination of Rewriting
A. Krauss (2011)
10.1007/s10817-011-9219-0
Strongly Typed Term Representations in Coq
N. Benton (2011)
10.1145/1086365.1086375
Combining programming with theorem proving
Chiyan Chen (2005)



This paper is referenced by
10.4230/DagRep.6.3.1
Data Structures and Advanced Models of Computation on Big Data (Dagstuhl Seminar 16101)
Alejandro López-Ortiz (2016)
Effectful Programming in Declarative Languages with an Emphasis on Non-Determinism: Applications and Formal Reasoning
Sandra Dylus (2020)
10.1145/3341708
Dijkstra monads for all
Kenji Maillard (2019)
10.1561/2500000045
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer (2019)
10.1109/BIGCOM.2019.00021
Formal Verification of BNB Smart Contract
X. Li (2019)
10.1145/2951913.2951932
Elaborator reflection: extending Idris in Idris
David Raymond Christiansen (2016)
10.1007/978-3-319-89884-1_9
Failure is Not an Option - An Exceptional Type Theory
Pierre-Marie Pédrot (2018)
10.1145/3064850
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
Colin S. Gordon (2017)
10.1145/3122955.3122963
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq
Niki Vazou (2017)
10.1007/978-3-319-89884-1_11
Behavioural Equivalence via Modalities for Algebraic Effects
Alex K. Simpson (2018)
10.1007/978-3-030-03427-6_15
Scalability of Deductive Verification Depends on Method Call Treatment
Alexander Knüppel (2018)
10.1145/3341707
A predicate transformer semantics for effects (functional pearl)
Wouter Swierstra (2019)
10.1145/3331554.3342607
Inductive types deconstructed: the calculus of united constructions
Stefan Monnier (2019)
LIO*: Low Level Information Flow Control in F
Jean-Joseph Marty (2020)
10.1007/978-3-030-28483-1_4
SMTCoq: Mixing Automatic and Interactive Proof Technologies
C. Keller (2019)
10.4230/LIPIcs.SNAPL.2017.1
Everest: Towards a Verified, Drop-in Replacement of HTTPS
K. Bhargavan (2017)
10.1145/3018610.3018618
Equivalence of system f and ź2 in Coq based on context morphism lemmas
Jonas Kaiser (2017)
10.1007/978-3-030-52482-1
Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings
Ivan Lanese (2020)
10.1109/MSP.2018.3761710
Quantum Computing: Codebreaking and Beyond
Martin Roetteler (2018)
Elaborator Reflection : Extending Idris in
D. Christiansen (2016)
10.1080/1206212X.2016.1253911
A fine-grained framework for quantifying secure management of state in object-oriented programs
A. Stewart (2017)
10.1109/EuroSPW.2018.8429049
Ledger design language: designing and deploying formally verified public ledgers
Nadim Kobeissi (2018)
On the security of authentication protocols on the web. (La sécurité des protocoles d'authentification sur leWeb)
Antoine Delignat-Lavaud (2016)
Méthodes et outils pour la spécification et la preuve de propriétés difficiles de programmes séquentiels
Martin Clochard (2018)
Monnier 2019 ] is a functional language based on a dependently typed calculus , in the tradition of Coq [
Stefan Monnier (2019)
Compilation using Correct-by-Construction Program Synthesis by Clément Pit-Claudel
Clément Pit-Claudel (2015)
10.1007/978-3-030-03332-3
Advances in Cryptology – ASIACRYPT 2018
Steven D. Galbraith (2018)
Adding dependent types to class-based mutable objects
J. C. Campos (2018)
10.1145/2980983.2908091
Occurrence typing modulo theories
Andrew M. Kent (2016)
Type system for resource bounds with type-preserving compilation
P. Wang (2019)
10.23919/FMCAD.2019.8894248
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
Faria Kalim (2019)
10.1007/978-3-030-03332-3_9
State Separation for Code-Based Game-Playing Proofs
Chris Brzuska (2018)
See more
Semantic Scholar Logo Some data provided by SemanticScholar