[Best viewed with any browser]


A simple functional language with a built-in theorem prover


FUNL is a simply typed functional programming language with integers, booleans, and primitive recursion over integers. It is implemented in Haskell using the Ivor proof engine. By using the same framework for the language implementation and the theorem prover, we can be sure that the language and theorem prover are always consistent with each other. This is a very small language, and a proof of concept for a larger implementation of a functional language with a built-in theorem prover.

Building and Running

You will need the Ivor proof engine for Haskell, which requires GHC version 6.4 or greater. To build, first install Ivor, download the sources (see below), and type 'make' in the source directory. This builds the executable funl.

There is a small example program, test.fnl, in the distribution. This includes some small functions, and statements of properties the functions should hold. Run './funl test.fnl and you will be presented with an interactive theorem proving interface for each property statement in the file. When all these are complete, you will be given an evaluation prompt.

Proof scripts for each property are given in test.fnl in comments.

TODO: (or perhaps exercises for the reader...)


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