{"id":169556,"date":"2008-05-29T08:34:41","date_gmt":"2008-05-29T15:34:41","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/project\/f7-refinement-types-for-f\/"},"modified":"2020-05-05T00:34:09","modified_gmt":"2020-05-05T07:34:09","slug":"f7-refinement-types-for-f","status":"publish","type":"msr-project","link":"https:\/\/www.microsoft.com\/en-us\/research\/project\/f7-refinement-types-for-f\/","title":{"rendered":"F7: Refinement Types for F#"},"content":{"rendered":"
F7 is an enhanced typechecker for the F#<\/a> programming language, a dialect of ML. F7 pioneers the static checking of security properties expressed with refinement types. Although the original motivation was to check security properties, F7 is not security-specific and is applied in other areas, such as database modelling.<\/p>\n The theoretical core of F7 is the typed lambda-calculus Refined Concurrent FPC, or RCF for short. FPC itself is Plotkin and Gunter’s lambda-calculus with function, sum, product, unit, and recursive types. Refinement types are types qualified by logical formulas, also known as subset types. For example, x:int {x>0}, is the type of positive integers. RCF consists of FPC plus refinement types, dependent function and pair types, and concurrency in the style of the pi-calculus.<\/p>\n The F7 implementation checks ordinary F# source code against enhanced F7 interface files. During typechecking F7 generates proof obligations that are passed to the Z3 SMT solver. The F7 download includes binaries, Visual Studio support, a range of sample protocols and libraries, and the source code of F7 itself.<\/p>\n Our work on checking F# implementations of cryptographic software with F7, builds on prior work on FS2PV, developed in the Samoa<\/a> project, which checks F# by compiling to the ProVerif<\/a> tool. F7 descends from the Cryptyc<\/a> typechecker, which used dependent types to analyze security protocols, but which checked abstract process calculus models rather than executable F# code. Together with other tools, F7 is a constituent of the Cryptographic Verification Kit (CVK) developed at MSR Cambridge<\/a> and the MSR-INRIA Joint Centre. The most substantial application of F7 is to the cryptographic verification of miTLS<\/a>, a reference implementation of TLS 1.2; miTLS consists of 5KLOC\u00a0in F# together 2.5KLOC of F7 interface annotations.\u00a0The use of refinement types in F7 was inspired by the Sage<\/a> programming language. Some related security-oriented programming languages include AURA<\/a> and Fine<\/a>, and Dsolve<\/a> is another recent system of refinement types for ML. The F5<\/a> tool-chain is an independent implementation of RCF, enriched with union, intersection, and polymorphic types. F*<\/a> is a more recent language that unifies and extends<\/a> most features of Fine and F7.<\/p>\n