An embedding of Fortran expressions into strongly-typed Haskell values, and facilities for reasoning about them.

Each Fortran type gets a corresponding Haskell type.

The Fortran expressions that can be formed are specified at the type level.

Fortran values and expressions are represented symbolically, in a form that can be easily used in external theorem-provers via Data.SBV.