free-compiler-0.3.0.0: A Haskell to Coq compiler.

This compiler converts Haskell code to Coq and Agda. Effectful Haskell code is modelled in Coq and Agda by applying a monadic transformation. We use the free monad for this purpose such that it is possible to reason about the code in an effect generic fashion. The Coq back end of the compiler can model sharing. The user can select at runtime between call-by-name, call-by-need and call-by-value semantics. The Agda back end is limited to call-by-name at the moment. This package is based on an early prototype developed at Flensburg University of Applied Sciences by Benedikt Jessen.