Semantic Purity and Effects Reunited in F* (Outdated)

Semantic Purity and Effects Reunited in F* (Outdated)

Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Pierre-Yves Strub, Aseem Rastogi,
Antoine Delignat-Lavaud, Karthikeyan Bhargavan, and Cédric Fournet

This draft was superseded by Dependent Types and Multi-Monadic Effects in F*


We present (new) F*, a dependently typed language for writing general-purpose programs with effects, specifying them within its functional core, and verifying them semi-automatically, by a combination of type inference, SMT solving, and manual proofs.
A central difficulty is to ensure the consistency of a core language of proofs within a larger language in which programs may exhibit effects such as state, exceptions, non-termination, IO, concurrency, etc. Prior attempts at solving this problem generally resort to a range of ad hoc methods. Instead, the main novelty of F* is to safely embrace and extend the familiar style of type-and-effect systems with fully dependent types.
F* is founded on a λ-calculus with a range of primitive effects and a dependent type system parameterized by a user-defined lattice of Dijkstra monads. For each monad, the user provides a predicate-transformer that captures its effective semantics. At the bottom of the lattice is a distinguished Pure monad, such that computations typeable as Pure are normalizing---our termination argument is based on well-founded relations and is fully semantic.
We illustrate our design on a series of challenging programming examples. We outline its metatheory on a core calculus, for which we prove soundness and termination of the Pure fragment. We also discuss selected aspects of its fresh typechecker. The F* system is open source; it fully supports our new design; it generates F# and OCaml code; and it bootstraps to several platforms.

Old Materials