Simple equational reasoning for a Haskell-ish language

Latest on Hackage:

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow to host generated Haddocks.

BSD3 licensed by Adam Procter and Aaron Stump
Maintained by Adam Procter

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 <>

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!


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.


comments powered byDisqus