A proof tool dedicated to clean the first prototype

Abstract

Theorem proving for functional programming languages can be made much easier by the availability of a dedicated theorem prover. A theorem prover is dedicated to a specific programming language when it fully supports the syntax and semantics of the language and offers specialized proving support for it. Using a dedicated theorem prover is easy, because one can reason about a developed program without having to translate it. However, no suited dedicated theorem prover for a functional language exists yet. This paper describes a simple prototype of a dedicated theorem prover for the functional language Clean. A description of the possibilities of the prototype is given and an examination is made of the work that needs to be done to extend the prototype to a fully operational and truly useful programming tool. Also example proofs of some basic properties and of a graph transformation are given.