Transforming Programs into Recursive Functions

This paper presents a new proof-assistant based approach to program verification: programs are translated, via fully-automatic deduction, into tail-recursive function defined in the logic of a theorem prover. This approach improves on well-established methods based on Hoare logic and verification condition generation (VCG) by removing the need to annotate programs with assertions, making the proof natural to the theorem prover and being easier to implement than a trusted VCG. Our tool has been implemented in the HOL4 theorem prover.