Readme for mprover-0.0.0.0
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/