F* (programming language)

From Wikipedia, the free encyclopedia
Jump to: navigation, search
FStar Logo.png
Paradigm multi-paradigm: functional, imperative, formal verification
Designed by Microsoft Research, MSR-Inria, and Inria
Preview release 39063dc / May 10, 2015 (2015-05-10)
Typing discipline static, strong, inferred, dependent types, formal verification
OS Cross-platform
License Apache 2.0 License
Website www.fstar-lang.org
Influenced by
F#, OCaml, Standard ML, Fine, F7, F5, FX, HTT, Trellys, Zombie, Dafny

F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system is based on a core that resembles System Fω (hence the name), but is extended with dependent types, monadic effects, and refinement types. Together, these features allow expressing precise specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml or F# for execution. Previous versions of F* could also be translated to JavaScript.

The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source (under the Apache 2.0 License) and is under active development on GitHub.


Swamy, Nikhil; Hriţcu, Cătălin; Keller, Chantal; Rastogi, Aseem; Delignat-Lavaud, Antoine; Forest, Simon; Bhargavan, Karthikeyan; Fournet, Cédric; Strub, Pierre-Yves; Kohlweiss, Markulf; Zinzindohoue, Jean-Karim (2015), Dependent Types and Multi-Monadic Effects in F* 

External links[edit]