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
make' in the source directory. This builds the
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 '
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
TODO: (or perhaps exercises for the reader...)
Edwin Brady -- email@example.com -- echo $modified; ?>