A Prototype Dedicated Theorem Prover for Clean

This paper examines an approach to computer assisted formal reasoning in relation to functional programming. Instead of using a generic proof tool which may differ on some points from the functional language used, a new proof tool is to be developed which is solely intended for proving properties of programs written in one specific language. This proof tool is intended to be inserted in the Integrated Development Environment of the programming language, which ensures a seamless integration. A prototype approximating such a proof tool for the pure, lazy functional programming language Clean has been implemented and will be described in this paper. It will be shown how this prototype can be used and examples of theorems that can be proven with it will be given. An examination will be made of the work that needs to be done to extend the prototype to an integrated programming tool.