F* (programming language)
F* (pronounced F star) is an ML-like functional programming languageaimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, and refinement types. Together, these features allow expressing precise specifications for programs, including functional correctness 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 or F# for execution. Previous versions of F* could also be translated to JavaScript.
Wikipage disambiguates
primaryTopic
F* (programming language)
F* (pronounced F star) is an ML-like functional programming languageaimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, and refinement types. Together, these features allow expressing precise specifications for programs, including functional correctness 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 or F# for execution. Previous versions of F* could also be translated to JavaScript.
has abstract
F* (pronounced F star) is an M ...... active development on GitHub.
@en
F*是一个由微软研究院开发的基于F♯的依赖类型函数式程序语言 ...... 较之于F#更加丰富，它允许可被半自动化检查的功能正确性规范。
@zh
influenced by
latest release version
repository
license
Link from a Wikipage to an external page
Wikipage page ID
38,420,593
Wikipage revision ID
730,960,192
designers
Microsoft Research, MSR-Inria, and Inria
operating system
paradigm
subject
hypernym
comment
F* (pronounced F star) is an M ...... o be translated to JavaScript.
@en
F*是一个由微软研究院开发的基于F♯的依赖类型函数式程序语言 ...... 较之于F#更加丰富，它允许可被半自动化检查的功能正确性规范。
@zh
label
F* (programming language)
@en
F*
@zh
wasDerivedFrom
depiction
isPrimaryTopicOf
name
F*
@en