Leonard Lensink, Marko van Eekelen
Abstract:
Sparkle is a proof assistant designed for the lazy
functional programming language Clean.
It is designed to facilitate proofs of first order
logical predicates on existing and newly written programs.
In order to achieve this it is of the utmost
importance that the proof system is easy to use and integrated into the IDE.
The implementation of Sparkle only has a basic
induction principle so far.
For many programs and complex proofs this will not
suffice.
To address this issue we have expanded Sparkle with
several induction and co-induction proof techniques for mutually recursive
functions and data types.
By providing examples of proofs on programs, taken
from various research papers, we show how the programmer can benefit from these
added tactics.
With our extensions Sparkle can be used to prove
properties of a wide class of programs.