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.
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...)
darcs get http://www-fp.dcs.st-and.ac.uk/~eb/darcs/Funl
.