mprover: Simple equational reasoning for a Haskell-ish language

[ bsd3, program, theorem-provers ] [ Propose Tags ]

MProver is a proof checker for equational reasoning in a Haskell-like language. This is an extremely preliminary release, so don't expect it to be terribly useful just yet!

[Skip to Readme]

Downloads

mprover-0.0.0.0.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

AdamProcter

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	0.0.0.0
Dependencies	base (<6), containers (>=0.4.0.0), haskell98, mtl (>=2.0.1.0), parsec (>=3.1.1), pretty (>=1.0.1.2), transformers (>=0.2.2.0), unbound (>=0.3.1) [details]
License	BSD-3-Clause
Author	Adam Procter and Aaron Stump
Maintainer	Adam Procter <amp269@mail.missouri.edu>
Category	Theorem Provers
Uploaded	by AdamProcter at 2011-12-15T11:14:55Z
Distributions
Reverse Dependencies	1 direct, 0 indirect [details]
Executables	mp
Downloads	984 total (6 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs not available [build log] All reported builds failed as of 2016-12-26 [all 8 reports]

Readme for mprover-0.0.0.0

[back to package description]

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/