The ivor package

[Tags:bsd3, deprecated, library]
Deprecated. in favor of idris

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.

Properties

Versions 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.3), containers, directory, haskell98 (<2), mtl, parsec [details]
License BSD3
Author Edwin Brady
Maintainer Edwin Brady <eb@dcs.st-and.ac.uk>
Stability experimental
Category Theorem provers, Dependent Types
Home page http://www.dcs.st-and.ac.uk/~eb/Ivor/
Uploaded Sun Jul 19 14:29:25 UTC 2009 by EdwinBrady
Updated Thu Feb 11 20:59:14 UTC 2016 by HerbertValerioRiedel to revision 1
Distributions NixOS:0.1.14.1
Downloads 1719 total (28 in the last 30 days)
Votes
0 []
Status Docs uploaded by user
Build status unknown [no reports yet]

Modules

[Index]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees