free-compiler

A Haskell to Coq compiler that represents effectful programs with the free monad

free-proving-code

Library to model effectful programs and prove properties about these programs in Coq

language-coq

Coq AST and pretty-printer written in Haskell

call-by-preference