Download | Documentation | Examples
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 (which I call TT) and tactics for building terms in the type theory, 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 in his thesis. The primary aim of Ivor is to support research in generative programming and resource bounded computation in Hume (see, e.g. this paper), but it is more generally applicable.
Unlike other systems, Ivor is intended to be used by programs, rather than a human operator. To this end, 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. See below for examples.
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.
The distribution includes a stand alone shell wrapper around the library, for experimental purposes. This shell can be extended with user tactics (see API documentation for details).
[Why Ivor? British people of a certain age will recognise the name of another kind of engine...]
You can also get the current version with git:
git clone git://github.com/edwinb/Ivor.git
Requires a recent version of GHC to build (I'm using 7.0.3).
An introductory paper is available, and the API is fully documented with haddock:
Som examples which can be pasted into the shell in the
examplett/ directory. The exported modules are
Ivor.TT (with the interface to the type theory and
Ivor.Primitives (which extends the type
theory with some primitive types),
(which exports parser combinators for terms and data types) and
Ivor.Shell (which allows a user program to drop into
shell mode, possibly extended by user defined tactics).
darcs get http://www-fp.dcs.st-and.ac.uk/~eb/darcs/Logic
This example shows how to use the library to implement a simple theorem prover; it creates several data types for representing connectives, and implements some simple tactics for constructing proofs of expressions in propositional logic. Documentation is provided at the command line.
STLC, an implementation of simply typed lambda calculus, using Ivor for the typechecker and evaluator, with a Haskell front end for parsing.
Funl, an implementation of a simple functional programming language with a built in theorem prover, using Ivor to construct well typed terms, deal with renaming issues, evaluate programs and build correctness proofs.
Edwin Brady -- email@example.com -- 19th July 2009