Languages Features Creators CSV Resources Challenges Add Language
GitHub icon


F* - Programming language

< >

F* is a programming language created in 2014.

#230on PLDB 9Years Old 3.4kUsers
0Books 1Papers 250Repos

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. Read more on Wikipedia...

Example from hello-world:
module Hello let main = FStar.IO.print_string "Hello World\n"

Keywords in F*

abstract attributes noeq unopteq andbegin by default effect else end ensures exception exists false forall fun function if in include inline inlineforextraction irreducible logic match module mutable new neweffect noextract of open opaque private rangeof reifiable reify reflectable requires setrangeof sub_effect synth then total true try type unfold unfoldable val when with not

Language features

Feature Supported Token Example
Binary Literals
Booleans true false
Print() Debugging FStar.IO.print_string

Publications about F* from Semantic Scholar

title authors year citations influentialCitations
Verified low-level programming embedded in F* Jonathan Protzenko and J. Zinzindohoué and Aseem Rastogi and T. Ramananandro and Peng Wang and Santiago Zanella Béguelin and Antoine Delignat-Lavaud and Catalin Hritcu and K. Bhargavan and C. Fournet and N. Swamy 2017 104 9
java-bytecode.html · fstar.html · clean.html

View source

- Build the next great programming language · Search · Day 213 · About · Blog · Acknowledgements · Traffic · Traffic Today · GitHub ·