Jump to content

F* (programming language)

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by 2600:1015:b026:2030:50aa:1072:8097:bb49 (talk) at 17:27, 22 February 2020 (Influences). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Not to be confused with F (programming language).
F*
ParadigmMulti-paradigm: functional, imperative
Designed byMicrosoft Research and Inria[1]
Stable release
Typing disciplineDependent, inferred, static, strong
OSLinux, macOS, Windows
LicenseApache License 2.0
Websitewww.fstar-lang.org
Influenced by
Coq, Dafny, F#, Lean, OCaml, Standard ML

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 both OCaml and F#. It is open source (under the Apache License 2.0) and is under active development on GitHub.[2]

References

  1. ^ "Microsoft Research Inria Joint Centre". MSR-INRIA.
  2. ^ "FStarLang/FStar". GitHub.

Sources

  • 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. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
  • 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. {{cite conference}}: Unknown parameter |booktitle= ignored (|book-title= suggested) (help)
Stub icon

This programming-language-related article is a stub. You can help Wikipedia by expanding it.

Retrieved from "https://en.wikipedia.org/w/index.php?title=F*_(programming_language)&oldid=942108618"