Movatterモバイル変換

[0]ホーム
URL:

Jump to content
WikipediaThe Free Encyclopedia
Search

F* (programming language)

From Wikipedia, the free encyclopedia
Functional programming language inspired by ML and aimed at program verification
Not to be confused withF (programming language) orF＃ (programming language).
F*
The official F* logo
ParadigmMulti-paradigm:functional,imperative
FamilyML:Caml:OCaml
Designed byNikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
DevelopersMicrosoft Research,
Inria[1]
First appeared2011; 14 years ago (2011)
Stable release
v2025.03.25[2] / 26 March 2025; 7 months ago (2025-03-26)
Typing disciplinedependent,inferred,static,strong
Implementation languageF*
OSCross-platform:Linux,macOS,Windows
LicenseApache 2.0
Filename extensions.fst
Websitefstar-lang.org
Influenced by
Dafny,F#,Lean,OCaml,Rocq,Standard ML

F* (pronouncedF star) is ahigh-level,multi-paradigm,functional andobject-orientedprogramming language inspired by the languagesML,Caml, andOCaml, and intended forprogram verification. It is a joint project ofMicrosoft Research, and theFrench Institute for Research in Computer Science and Automation (Inria).[1] Itstype system includesdependent types,monadiceffects, andrefinement 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 ofsatisfiability modulo theories (SMT) solving andmanual proofs. For execution, programs written in F* can be translated toOCaml,F#,C,WebAssembly (via KaRaMeL tool), orassembly language (via Vale toolchain). Prior F* versions could also be translated toJavaScript.

It was introduced in 2011.[3][4] and is under active development onGitHub.[2]

History

[edit]

Versions

[edit]

Until version 2022.03.24, F* was written entirely in a common subset of F* andF# and supported bootstrapping in bothOCaml and F#. This was dropped starting in version 2022.04.02.[5][6]

Overview

[edit]

Operators

[edit]

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

Data types

[edit]

Common primitivedata types in F* arebool,int,float,char, andunit.[7]

References

[edit]
  1. ^ab"Microsoft Research Inria Joint Centre".MSR-INRIA.
  2. ^ab"FStarLang/FStar".GitHub. Retrieved18 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. Retrieved17 April 2023.
  4. ^"The F* Project".Microsoft. Retrieved20 April 2023.
  5. ^"fstar.exe is no longer buildable in F# as a .NET executable #2512".Github. Retrieved17 April 2023.
  6. ^"Consider dropping requirement that F* code has to be valid F# #1737".Github. Retrieved17 April 2023.
  7. ^abSwamy, Nikhil; Martínez, Guido; Rastogi, Aseem (Jan 14, 2024).Proof-Oriented Programming in F*(PDF).

Sources

[edit]
  • 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.
  • Swamy, Nikhil; Martínez, Guido; Rastogi, Aseem (2024).Proof-Oriented Programming in F*.

External links

[edit]
ML programming
Software
Implementations,
dialects
Caml
Standard ML
Dependent ML
Programming tools
Theorem provers,
proof assistants
Community
Designers
  • Lennart Augustsson (Lazy ML)
  • Damien Doligez (OCaml)
  • Gérard Huet (Caml)
  • Xavier Leroy (Caml, OCaml)
  • Robin Milner (ML)
  • Don Sannella (Extended ML)
  • Don Syme (F#)
    • Overview
    Software
    Applications
    Video games
    Programming
    languages
    Frameworks,
    development tools
    Operating systems
    Other
    Licenses
    Forges
    Related
    Microsoft development tools
    Development
    environments
    Visual Studio
    Others
    Languages
    APIs and
    frameworks
    Native
    .NET
    Device drivers
    Database
    SQL Server
    SQL services
    Other
    Source control
    Testing and
    debugging
    Delivery
    Main
    projects
    Languages, compilers
    Distributed–grid computing
    Internet,networking
    Other projects
    Operating systems
    APIs
    Launched as products
    MSR Labs
    applied
    research
    Live Labs
    Current
    Discontinued
    FUSE Labs
    Other labs
    Retrieved from "https://en.wikipedia.org/w/index.php?title=F*_(programming_language)&oldid=1309662244"
    Categories:
    Hidden categories:
    [8]ページ先頭
    ©2009-2025 Movatter.jp