A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://en.wikipedia.org/wiki/F*_(programming_language) below:

F* (programming language) - Wikipedia

From Wikipedia, the free encyclopedia

Functional programming language inspired by ML and aimed at program verification

F*

The official F* logo

Paradigm Multi-paradigm: functional, imperative Family ML: Caml: OCaml Designed by Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang Developers Microsoft Research,
Inria[1] First appeared 2011; 14 years ago (2011) Stable release

v2025.03.25

[2]

/ 26 March 2025

; 3 months ago (2025-03-26) Typing discipline dependent, inferred, static, strong Implementation language F* OS Cross-platform: Linux, macOS, Windows License Apache 2.0 Filename extensions .fst Website fstar-lang.org Dafny, F#, Lean, OCaml, Rocq, Standard ML

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).[1] 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.[3][4] and is under active development on GitHub.[2]

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.[5][6]

F* supports common arithmetic operators such as +, -, *, and /. Also, F* supports relational operators like <, <=, ==, !=, >, and >=.[7]

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

  1. ^ a b "Microsoft Research Inria Joint Centre". MSR-INRIA.
  2. ^ a b "FStarLang/FStar". GitHub. Retrieved 18 May 2025.
  3. ^ Swamy, Nikhil; Chen, Juan; Fournet, Cédric; Strub, Pierre-Yves; Bhargavan, Karthikeyan; Yang, Jean (September 2011). Secure distributed programming with value-dependent types. ICFP '11: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. Vol. 46. Tokyo, Japan: Association for Computing Machinery. pp. 266–278. doi:10.1145/2034574.2034811. Retrieved 17 April 2023.
  4. ^ "The F* Project". Microsoft. Retrieved 20 April 2023.
  5. ^ "fstar.exe is no longer buildable in F# as a .NET executable #2512". Github. Retrieved 17 April 2023.
  6. ^ "Consider dropping requirement that F* code has to be valid F# #1737". Github. Retrieved 17 April 2023.
  7. ^ a b Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (Jan 14, 2024). Proof-Oriented Programming in F* (PDF).

RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4