×

F*

swMATH ID: 27563
Software Authors: Microsoft Research, INRIA; Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean
Description: F* (pronounced F star) is a general-purpose functional programming language with effects aimed at program verification. It puts together the automation of an SMT-backed deductive verification tool with the expressive power of a proof assistant based on dependent types. After verification, F* programs can be extracted to efficient OCaml, F#, C or ASM code. This enables verifying the functional correctness and security of realistic applications. The main ongoing use case of F* is building a verified, drop-in replacement for the whole HTTPS stack in Project Everest. This includes verified implementations of TLS 1.2 and 1.3 and of the underlying cryptographic primitives. F*’s type system includes dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness and security properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and interactive proofs.
Homepage: https://www.fstar-lang.org/
Source Code:  https://github.com/FStarLang/FStar
Related Software: Coq; AURA; Nuprl; EasyCrypt; Idris; Irdis; z3; Agda; Zoo Probabilistic Systems; Lifting; Transfer; Autoref; Isabelle/HOL; JFlow; Fable; Why3; Links; JavaScript; ProVerif; Cayenne
Cited in: 21 Documents
Further Publications: https://www.fstar-lang.org/#papers

Citations by Year