F* (programming language)

---

title: "F* (programming language)" type: doc version: 1 created: 2026-02-28 author: "Wikipedia contributors" status: active scope: public tags: ["high-level-programming-languages", "functional-languages", "ocaml-programming-language-family", ".net-programming-languages", "microsoft-programming-languages", "microsoft-research", "microsoft-free-software", "dependently-typed-languages", "automated-theorem-proving", "programming-languages-created-in-2011", "proof-assistants", "2011-software", "cross-platform-free-software", "software-using-the-apache-license", "statically-typed-programming-languages"] description: "Functional programming language inspired by ML and aimed at program verification" topic_path: "technology/programming-languages" source: "https://en.wikipedia.org/wiki/F*_(programming_language)" license: "CC BY-SA 4.0" wikipedia_page_id: 0 wikipedia_revision_id: 0

::summary Functional programming language inspired by ML and aimed at program verification ::

::data[format=table title="Infobox programming language"]

Field	Value
name	F*
logo	Fstar-official-logo-2015.png
logo size	128px
logo caption	The official F* logo
paradigm	Multi-paradigm: functional, imperative
family	ML: Caml: OCaml
designers	Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
developers	Microsoft Research,
Inria
released
latest release version	v2025.03.25
latest release date
typing	dependent, inferred, static, strong
programming language	F*
operating system	Cross-platform: Linux, macOS, Windows
license	Apache 2.0
website
file ext	.fst
influenced by	Dafny, F#, Lean, OCaml, Rocq, Standard ML
::

| name = F* | logo = Fstar-official-logo-2015.png | logo size = 128px | logo caption = The official F* logo | paradigm = Multi-paradigm: functional, imperative | family = ML: Caml: OCaml | designers = Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang | developers = Microsoft Research, Inria | released = | latest release version = v2025.03.25 | latest release date = | typing = dependent, inferred, static, strong | programming language = F* | operating system = Cross-platform: Linux, macOS, Windows | license = Apache 2.0 | website = | file ext = .fst | implementations = | dialects = | influenced by = Dafny, F#, Lean, OCaml, Rocq, Standard ML | influenced =

F* (pronounced F star) is a high-level, multi-paradigm, functional and object-oriented programming language inspired by the languages ML, Caml, and OCaml, and intended for program verification. It is a joint project of Microsoft Research, and the French Institute for Research in Computer Science and Automation (Inria). 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 satisfiability modulo theories (SMT) solving and manual proofs. For execution, programs written in F* can be translated to OCaml, F#, C, WebAssembly (via KaRaMeL tool), or assembly language (via Vale toolchain). Prior F* versions could also be translated to JavaScript.

It was introduced in 2011 |last1=Swamy |first1=Nikhil |last2=Chen |first2=Juan |last3=Fournet |first3=Cédric |last4=Strub |first4=Pierre-Yves |last5=Bhargavan |first5=Karthikeyan |last6=Yang |first6=Jean |date=September 2011 |title=Secure distributed programming with value-dependent types |conference=ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming |volume=46 |issue=9 |pages=266–278 |location=Tokyo, Japan |doi=10.1145/2034574.2034811 |publisher=Association for Computing Machinery |url=https://dl.acm.org/doi/10.1145/2034773.2034811 |access-date=17 April 2023|url-access=subscription

History

Versions

Until version 2022.03.24, F* was written entirely in a common subset of F* and F# and supported bootstrapping in both OCaml and F#. This was dropped starting in version 2022.04.02.

Overview

Operators

F* supports common arithmetic operators such as +, -, *, and /. Also, F* supports relational operators like ``, and =.

Data types

Common primitive data types in F* are bool, int, float, char, and unit.

References

Sources

• {{cite conference |last1=Ahman |first1=Danel |last2=Hriţcu |first2=Cătălin |last3=Maillard |first3=Kenji |last4=Martínez |first4=Guido |last5=Plotkin |first5=Gordon |last6=Protzenko |first6=Jonathan |last7=Rastogi |first7=Aseem |last8=Swamy |first8=Nikhil |year=2017 |title=Dijkstra Monads for Free |url=https://fstar-lang.org/papers/dm4free/ |book-title=44nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• {{cite conference |last1=Swamy |first1=Nikhil |last2=Hriţcu |first2=Cătălin |last3=Keller |first3=Chantal |last4=Rastogi |first4=Aseem |last5=Delignat-Lavaud |first5=Antoine |last6=Forest |first6=Simon |last7=Bhargavan |first7=Karthikeyan |last8=Fournet |first8=Cédric |last9=Strub |first9=Pierre-Yves |last10=Kohlweiss |first10=Markulf |last11=Zinzindohoue |first11=Jean-Karim |last12=Zanella-Béguelin |first12=Santiago |year=2016 |title=Dependent Types and Multi-Monadic Effects in F* |url=https://fstar-lang.org/papers/mumon/ |book-title=43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
• Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024). Proof-Oriented Programming in F*.

References

1. "Microsoft Research Inria Joint Centre".
2. "The F* Project".
3. "FStarLang/FStar".
4. "fstar.exe is no longer buildable in F# as a .NET executable #2512".
5. "Consider dropping requirement that F* code has to be valid F# #1737".
6. Swamy, Nikhil. (Jan 14, 2024). "Proof-Oriented Programming in F*".

::callout[type=info title="Wikipedia Source"] This article was imported from Wikipedia and is available under the Creative Commons Attribution-ShareAlike 4.0 License. Content has been adapted to SurfDoc format. Original contributors can be found on the article history page. ::