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

F*

F*

F* is a pl created in 2014.

#223on PLDB 8Years 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 inline_for_extraction irreducible logic match module mutable new new_effect noextract of open opaque private range_of reifiable reify reflectable requires set_range_of sub_effect synth then total true try type unfold unfoldable val when with not

Language features

Feature Supported Example Token
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
j.html · fstar.html · ceylon.html

View source

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