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
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
Parameterised notions of computation
Robert Atkey (2009)
Dafny: An Automatic Program Verifier for Functional Correctness
K. Leino (2010)
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)
Towards a Mathematical Science of Computation
J. McCarthy (1962)
foetus - Termination Checker for Simple Functional Programs
A. Abel (2002)
Computational lambda-calculus and monads
E. Moggi (1989)
Type-based termination of recursive definitions
G. Barthe (2004)
Liquid types
P. M. Rondon (2008)
Authenticated-encryption with associated-data
P. Rogaway (2002)
Simple General Recursion in Type Theory
A. Bove (2001)
Report on the programming language Euclid
B. Lampson (1977)
Modular verification of security protocol code by typing
K. Bhargavan (2010)
Verifying higher-order programs with the dijkstra monad
N. Swamy (2013)
Hoare type theory, polymorphism and separation
Aleksandar Nanevski (2008)
Monadic Presentations of Lambda Terms Using Generalized Inductive Types
Thorsten Altenkirch (1999)
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)
Programming and reasoning with algebraic effects and dependent types
E. Brady (2013)
Reasoning about Aliasing
M. Utting (1996)
Region-based Memory Management
M. Tofte (1997)
Extraction in Coq: An Overview
Pierre Letouzey (2008)
The Coq development team. The Coq proof assistant
Cayenne—a language with dependent types
L. Augustsson (1998)
Formalized Metatheory with Terms Represented by an Indexed Family of Types
R. Adams (2004)
Mtac: a monad for typed tactic programming in Coq
Beta Ziliani (2013)
Secure distributed programming with value-dependent types
N. Swamy (2011)
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
S. Schäfer (2015)
Combining proofs and programs in a dependently typed language
Chris Casinghino (2014)
Implementing Mathematics with the Nuprl
R. L. Constable (1986)
Subtypes for Specifications: Predicate Subtyping in PVS
J. Rushby (1998)
Practical Foundations for Programming Languages
R. Harper (2012)
Why3 - Where Programs Meet Provers
J. Filliâtre (2013)
Refinement types for ML
Timothy S. Freeman (1991)
Implementing TLS with Verified Cryptographic Security
K. Bhargavan (2013)
Refinement types for Haskell
R. Jhala (2014)
Implementing mathematics with the Nuprl proof development system
R. Constable (1986)
Guarded commands, nondeterminacy and formal derivation of programs
E. Dijkstra (1975)
Equational reasoning about programs with general recursion and call-by-value semantics
Garrin Kimmell (2012)
Subset Coercions in Coq
Matthieu Sozeau (2006)
Coq extraction, an overview
P Letouzey (2008)
Termination of Isabelle Functions via Termination of Rewriting
A. Krauss (2011)
Strongly Typed Term Representations in Coq
N. Benton (2011)
Combining programming with theorem proving
Chiyan Chen (2005)

This paper is referenced by
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)
Dijkstra monads for all
Kenji Maillard (2019)
QED at Large: A Survey of Engineering of Formally Verified Software
Talia Ringer (2019)
Formal Verification of BNB Smart Contract
X. Li (2019)
Elaborator reflection: extending Idris in Idris
David Raymond Christiansen (2016)
Failure is Not an Option - An Exceptional Type Theory
Pierre-Marie Pédrot (2018)
Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement Types
Colin S. Gordon (2017)
A tale of two provers: verifying monoidal string matching in liquid Haskell and Coq
Niki Vazou (2017)
Behavioural Equivalence via Modalities for Algebraic Effects
Alex K. Simpson (2018)
Scalability of Deductive Verification Depends on Method Call Treatment
Alexander Knüppel (2018)
A predicate transformer semantics for effects (functional pearl)
Wouter Swierstra (2019)
Inductive types deconstructed: the calculus of united constructions
Stefan Monnier (2019)
LIO*: Low Level Information Flow Control in F
Jean-Joseph Marty (2020)
SMTCoq: Mixing Automatic and Interactive Proof Technologies
C. Keller (2019)
Everest: Towards a Verified, Drop-in Replacement of HTTPS
K. Bhargavan (2017)
Equivalence of system f and ź2 in Coq based on context morphism lemmas
Jonas Kaiser (2017)
Reversible Computation: 12th International Conference, RC 2020, Oslo, Norway, July 9-10, 2020, Proceedings
Ivan Lanese (2020)
Quantum Computing: Codebreaking and Beyond
Martin Roetteler (2018)
Elaborator Reflection : Extending Idris in
D. Christiansen (2016)
A fine-grained framework for quantifying secure management of state in object-oriented programs
A. Stewart (2017)
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)
Advances in Cryptology – ASIACRYPT 2018
Steven D. Galbraith (2018)
Adding dependent types to class-based mutable objects
J. C. Campos (2018)
Occurrence typing modulo theories
Andrew M. Kent (2016)
Type system for resource bounds with type-preserving compilation
P. Wang (2019)
Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity
Faria Kalim (2019)
State Separation for Code-Based Game-Playing Proofs
Chris Brzuska (2018)
See more
Semantic Scholar Logo Some data provided by SemanticScholar