F* (programming language)

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
Paradigm multi-paradigm: functional, imperative, formal verification
Designed by Microsoft Research, MSR-Inria,[1] and Inria
Stable release
Typing discipline static, strong, inferred, dependent types, formal verification
OS Cross-platform
(Windows, macOS, and Linux)
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 a functional programming language inspired by ML and aimed at program verification. Its type system includes dependent types, monadic effects, and refinement types. This allows expressing precise 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 manual proofs. Programs written in F* can be translated to OCaml, F#, and C for execution. Previous versions of F* could also be translated to JavaScript.

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



  • Ahman, Danel; Hriţcu, Cătălin; Maillard, Kenji; Martínez, Guido; Plotkin, Gordon; Protzenko, Jonathan; Rastogi, Aseem; Swamy, Nikhil (2017). "Dijkstra Monads for Free". 44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 
  • 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; Zanella-Béguelin, Santiago (2016). "Dependent Types and Multi-Monadic Effects in F*". 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 

External links[edit]