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...]

- Version source (gpg signature)
- Via hackage.

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).

### Documentation

An introductory paper is available, and the API is fully documented
with haddock:

- Draft paper,
introducing the library with some simple example applications
(comments welcome).
- API documentation. Automatically generated
from the source by 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
tactics), `Ivor.Primitives`

(which extends the type
theory with some primitive types), `Ivor.TermParser`

(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).

### Examples

#### Propositional logic theorem prover

- Haskell source
- LogicDemo.lhs (main program; just
for browsing)

```
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.

#### Simply Typed Lambda Calculus

STLC, an implementation of simply typed lambda
calculus, using Ivor for the typechecker and evaluator, with a Haskell
front end for parsing.

#### Funl

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.