[Best viewed with any browser]

Ivor

A type theory based theorem proving library

Download | Documentation | Examples

Introduction

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

Download

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:

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

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.


Edwin Brady -- eb@cs.st-andrews.ac.uk --