PLDB
Languages Features Calendar CSV Lists Blog About Donate Add Language
GitHub icon

F*

< >

F* is a programming language created in 2014.

#235on 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
Integers
Floats
Hexadecimals
Octals
Conditionals
Functions
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
turtle.html · fstar.html · object-pascal.html

View source

PLDB - Build the next great programming language · v2023 · Day 153 · Docs · Build · Acknowledgements · Traffic Today · Traffic Trends · Mirrors · GitHub · feedback@pldb.com