ivor: Theorem proving library based on dependent type theory
Ivor is a type theory based theorem prover, with a Haskell API, designed for easy extending and embedding of theorem proving technology in Haskell applications. It provides an implementation of the type theory and tactics for building terms, more or less along the lines of systems such as Coq or Agda, and taking much of its inspiration from Conor McBride's presentation of OLEG.
The API provides a collection of primitive tactics and combinators for building new tactics. It is therefore possible to build new tactics to suit specific applications. Ivor features a dependent type theory similar to Luo's ECC with definitions (and similar to that implemented in Epigram), with dependent pattern matching, and experimental multi-stage programming support. Optionally, it can be extended with heterogeneous equality, primitive types and operations, new parser rules, user defined tactics and (if you want your proofs to be untrustworthy) a fixpoint combinator.
Modules
- Ivor
- Ivor.Construction
- Ivor.CtxtTT
- Ivor.Equality
- Ivor.EvalTT
- Ivor.Plugin
- Ivor.Primitives
- Ivor.Shell
- Ivor.TT
- Ivor.TermParser
- Ivor.ViewTerm
Downloads
- ivor-0.1.14.1.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)
Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.
Maintainer's Corner
For package maintainers and hackage trustees
Candidates
- No Candidates
Versions [RSS] | 0.1.5, 0.1.8, 0.1.9, 0.1.10, 0.1.10.1, 0.1.11, 0.1.12, 0.1.14, 0.1.14.1 |
---|---|
Dependencies | base (>=3 && <4.4), binary, containers, directory, haskell98 (<2), mtl, parsec [details] |
License | BSD-3-Clause |
Author | Edwin Brady |
Maintainer | Edwin Brady <eb@dcs.st-and.ac.uk> |
Revised | Revision 1 made by HerbertValerioRiedel at 2016-02-11T20:57:51Z |
Category | Theorem provers, Dependent Types |
Home page | http://www.dcs.st-and.ac.uk/~eb/Ivor/ |
Uploaded | by EdwinBrady at 2011-06-16T12:05:10Z |
Distributions | |
Reverse Dependencies | 2 direct, 0 indirect [details] |
Downloads | 8490 total (11 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-11-28 [all 8 reports] |