F* 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). 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, or assembly language. Prior F* versions could also be translated to JavaScript. Wikipedia

Developed by: Institut National de Recherche en Informatique et en Automatique • Microsoft Research
Operating systems: cross-platform
Implemented in: F#
Aliases: Fstar, F star, FStar

Wikidata: Q5423569

Influenced by: Dafny • F# • Lean • OCaml • Standard ML

Programming paradigms: functional programming • imperative programming

Language types: dependently typed programming language