Dependent Types and Multi-monadic Effects in F☆

被引:182
作者
Swamy, Nikhil [1 ]
Hritcu, Catalin [2 ]
Keller, Chantal [1 ,3 ]
Rastogi, Aseem [4 ]
Delignat-Lavaud, Antoine [2 ,5 ]
Forest, Simon [2 ,5 ]
Bhargavan, Karthikeyan [2 ]
Fournet, Cedric [1 ,3 ]
Strub, Pierre-Yves [6 ]
Kohlweiss, Markulf [1 ]
Zinzindohoue, Jean-Karim [2 ,5 ]
Zanella-Beguelin, Santiago [1 ]
机构
[1] Microsoft Res, Bangalore, Karnataka, India
[2] Inria, Rennes, France
[3] MSR Inria, Rennes, France
[4] UMD, Rennes, France
[5] ENS Paris, Paris, France
[6] IMDEA Software Inst, Paris, France
关键词
verification; proof assistants; effectful programming;
D O I
10.1145/2914770.2837655
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We present a new, completely redesigned, version of F-star, 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-star 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-star 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-star 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-star we have authored in the last year, focusing on three main case studies. Showcasing its use as a general-purpose programming language, F-star is programmed (but not verified) in F-star, and bootstraps in both OCaml and F#. Our experience confirms F-star'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-star 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-star than in a prior verified implementation of TLS-1.2. Finally, as a proof assistant, we discuss our use of F-star in mechanizing the metatheory of a range of lambda calculi, starting from the simply typed lambda calculus to System F-omega and even mu F-star, a sizeable fragment of F-star itself these proofs make essential use of F-star's flexible combination of SMT automation and constructive proofs, enabling a tactic-free style of programming and proving at a relatively large scale.
引用
收藏
页码:256 / 270
页数:15
相关论文
共 42 条
[1]  
Abel A., 1998, 474 LMU PROGR LAB
[2]  
Abel A., 2007, THESIS LMU MUNCHEN
[3]  
Adams R., 2006, TYP PROOFS PROGR INT
[4]  
Altenkirch T., 1999, COMP SCI LOG 13 INT
[5]  
[Anonymous], 2008, TRANSPORT LAYER SECU
[6]  
[Anonymous], COQ PROOF ASS
[7]   Parameterised notions of computation [J].
Atkey, Robert .
JOURNAL OF FUNCTIONAL PROGRAMMING, 2009, 19 :335-376
[8]  
Augustsson L., 1998, P 3 ACM SIGPLAN INT
[9]   Type-based termination of recursive definitions [J].
Barthe, G ;
Frade, MJ ;
Giménez, E ;
Pinto, L ;
Uustalu, T .
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2004, 14 (01) :97-141
[10]   Strongly Typed Term Representations in Coq [J].
Benton, Nick ;
Hur, Chung-Kil ;
Kennedy, Andrew J. ;
McBride, Conor .
JOURNAL OF AUTOMATED REASONING, 2012, 49 (02) :141-159