@hackage mprover0.0.0.0

Simple equational reasoning for a Haskell-ish language

  • Categories

    • License

      BSD-3-Clause

    • Maintainer

      Adam Procter <amp269@mail.missouri.edu>

    • Links

    • Versions

    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/