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...
module Hello
let main = FStar.IO.print_string "Hello World\n"
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
Feature | Supported | Token | Example |
---|---|---|---|
Binary Literals | ✓ | ||
Integers | ✓ | ||
Floats | ✓ | ||
Hexadecimals | ✓ | ||
Octals | ✓ | ||
Conditionals | ✓ | ||
Functions | ✓ | ||
Booleans | ✓ | true false | |
Print() Debugging | ✓ | FStar.IO.print_string |
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 |