Steps towards mechanizing program transformations using PVS

PVS is a highly automated framework for specification and verification. We show how the language and deduction features of PVS can be used to formalize, mechanize, and apply some useful program transformation techniques. We examine two such examples in detail. The first is a fusion theorem due to Bird where the composition of a catamorphism (a recursive operation on the structure of a datatype) and an anamorphism (an operation that constructs instances of the datatype) are fused to eliminate the intermediate data structure. The second example is Wandʹs continuation-based transformation technique for deriving tail-recursive functions from non-tailrecursive ones. These examples illustrate the utility of the language and inference features of PVS in capturing these transformations in a simple, general, and useful form.