A prototype dedicated theorem prover for Clean
M.J. de Mol, M.C.J.D. van Eekelen · 1998
Abstract. This paper examines an approach to computer assisted for-mal reasoning in relation to functional programming. Instead of using a generic proof tool which may differ on some points from the func-tional language used, a new proof tool is to be developed which is solely intended for proving properties of programs written in one specific lan-guage. This proof tool is intended to be inserted in the Integrated De-velopment 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 imple-mented 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. 1