@hackage / mprover

mprover-0.0.0.0

This is a highly preliminary release of MProver, a simple (I hope!) proof checker for equational reasoning in (a subset of) Haskell. It is released in the spirit, though not under the exact terms, of the CRAPL[1].

To build and install, use the standard incantation, viz.:

$ runhaskell Setup.hs configure $ runhaskell Setup.hs build $ runhaskell Setup.hs install

To launch the REPL (note that loading modules for use in the REPL is not supported yet, so you may find this a bit useless):

$ mp

To run the proof checker against an example MProver script:

$ mp examples/Test.hs

If you have any questions or comments, please write:

Adam Procter amp269@mail.missouri.edu

In particular, I'd be glad to send you a draft copy of a conference paper, currently under review, that outlines MProver's design.

Enjoy at your own risk!

Bugs/Limitations

Some particular bugs/limitations/to-do items of note:

• The guardedness check is not implemented yet.
• Program terms are not type checked (!)
• Type classes are not implemented yet.
• Case-proofs must be exhaustive; this is not actually checked for yet.

---

[1] http://matt.might.net/articles/crapl/