Introduction

F* (pronounced F star) is an ML-like functional programming language aimed at program verification. Its type system includes polymorphism, dependent types, monadic effects, refinement types, and a weakest precondition calculus. Together, these features allow expressing precise and compact specifications for programs, including functional correctness properties. The F* type-checker aims to prove that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml or F# for execution.

The latest version of F* is written entirely in F*, and bootstraps in OCaml and F#. It is open source and under active development on GitHub. A detailed description of this new F* version is available in a POPL 2016 paper. You can learn more about F* by following the online tutorial. Our recent ML workshop and HOPE talks on F* are available on YouTube.

Previous versions of F* could also be translated to JavaScript. We have used these previous versions in a number of projects, ranging from verifying implementations of cryptographic constructions and protocols, implementations of web browser extensions, formalizing the semantics of other languages (including JavaScript and a compiler from a subset of F* to JavaScript, and TS*, a secure subset of TypeScript), and even certifying the correctness of the core of F* type-checker itself.

Download

The sources of F* are hosted on GitHub. Binary packages are available for multiple platforms.

License

F* is distributed under the Apache 2.0 license.

F* Tutorial

Click the image below to start the F* tutorial.

F* Tutorial

Support

F* is a state-of-the-art research project under active development; as such, it contains a number of known bugs.

If you encounter a problem with F*, we encourage you to report it to the GitHub issue tracker. Please understand that we may not have the necessary manpower to address new feature requests - as an open source project, we welcome your contributions to help improve F*.

People

F* is a joint project between MSR Redmond, MSR Cambridge, the MSR-INRIA joint center, and INRIA. We have had many interns and collaborators from other institutions work on F* as well.

Current team

  • Aseem Rastogi (University of Maryland)
  • Nikhil Swamy (MSR Redmond)
  • Santiago Zanella-Béguelin (MSR Cambridge)
  • Jean-Karim Zinzindohoue (INRIA)

Past contributors


Papers

9 results
2016
[9] Dependent Types and Multi-Monadic Effects in F* (, , , , , , , , , , , ), In 43nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, . [bibtex] [pdf]
2015
[8] Wys*: A Verified Language Extension for Secure Multi-party Computations (, , ), . [bibtex] [pdf]
2014
[7] Gradual typing embedded securely in JavaScript (, , , , , , ), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Suresh Jagannathan, Peter Sewell, eds.), ACM, . [bibtex] [pdf] [doi]
[6] Probabilistic relational verification for cryptographic implementations (, , , , , ), In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Suresh Jagannathan, Peter Sewell, eds.), ACM, . [bibtex] [pdf] [doi]
2013
[5] Fully Abstract Compilation to JavaScript (, , , , , ), In 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, . [bibtex] [pdf]
[4] Verifying Higher-order Programs with the Dijkstra Monad (, , , , ), In Proceedings of the 34th annual ACM SIGPLAN conference on Programming Language Design and Implementation, . [bibtex] [pdf]
[3] Secure distributed programming with value-dependent types (, , , , , ), In J. Funct. Program., volume 23, . [bibtex] [pdf]
2012
[2] Self-Certification: Bootstrapping Certified Typecheckers in F* with Coq (, , , ), In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, . [bibtex] [pdf]
2011
[1] Secure distributed programming with value-dependent types (, , , , , ), In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming (Manuel M. T. Chakravarty, Zhenjiang Hu, Olivier Danvy, eds.), ACM, . [bibtex] [pdf] [doi]

Talks