F* (programming language)
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.
- Comment
- enF* (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.
- Depiction
- Designers
- enMicrosoft Research and Inria
- DifferentFrom
- F (programming language)
- FileExt
- en.fst
- Has abstract
- enF* (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.
- Homepage
- www.fstar-lang.org/
- Hypernym
- Programming
- InfluencedBy
- Coq
- Dafny (programming language)
- F Sharp (programming language)
- Lean (proof assistant)
- OCaml
- Standard ML
- Is primary topic of
- F* (programming language)
- Label
- enF* (programming language)
- LatestReleaseVersion
- FStar
- License
- Apache License 2.0
- Link from a Wikipage to an external page
- github.com/FStarLang/FStar
- www.fstar-lang.org/
- www.fstar-lang.org/papers/dm4free/
- www.fstar-lang.org/papers/mumon/
- www.fstar-lang.org/tutorial/
- Link from a Wikipage to another Wikipage
- Apache License 2.0
- C (programming language)
- Category:.NET programming languages
- Category:2013 software
- Category:Automated theorem proving
- Category:Dependently typed languages
- Category:Functional languages
- Category:Microsoft programming languages
- Category:Microsoft Research
- Category:ML programming language family
- Category:Programming languages created in 2013
- Category:Proof assistants
- Coq
- Dafny (programming language)
- Dependent types
- F Sharp (programming language)
- Functional programming
- Functional programming language
- GitHub
- Imperative programming
- Inria
- JavaScript
- Lean (proof assistant)
- Linux
- MacOS
- Microsoft Research
- ML (programming language)
- Monad (functional programming)
- Multi-paradigm programming language
- OCaml
- Program verification
- Proof assistant
- Refinement type
- Satisfiability modulo theories
- Side effect (computer science)
- Standard ML
- Static typing
- Strong typing
- Type inference
- Windows
- Logo
- enFstar-official-logo-2015.png
- LogoSize
- 128
- Name
- enF*
- OperatingSystem
- Linux
- MacOS
- Windows
- Paradigm
- Functional programming
- Imperative programming
- Multi-paradigm programming language
- SameAs
- 4jf4u
- F*
- F*
- F*
- F*
- F* (programming language)
- F* (プログラミング言語)
- m.0ql079r
- Q5423569
- Subject
- Category:.NET programming languages
- Category:2013 software
- Category:Automated theorem proving
- Category:Dependently typed languages
- Category:Functional languages
- Category:Microsoft programming languages
- Category:Microsoft Research
- Category:ML programming language family
- Category:Programming languages created in 2013
- Category:Proof assistants
- Thumbnail
- Typing
- Dependent types
- Static typing
- Strong typing
- Type inference
- WasDerivedFrom
- F* (programming language)?oldid=1119642763&ns=0
- Website
- https://www.fstar-lang.org/
- WikiPageLength
- 4714
- Wikipage page ID
- 38420593
- Wikipage revision ID
- 1119642763
- WikiPageUsesTemplate
- Template:Cite conference
- Template:Distinguish
- Template:Infobox programming language
- Template:Microsoft development tools
- Template:Microsoft FOSS
- Template:Microsoft Research
- Template:Prog-lang-stub
- Template:Reflist
- Template:Short description