Use of proof plans for transformation of functional programs by changes of data type

Program transformation concerns the derivation of an efficient program by applying correctness-preserving manipulations to a source program. Transformation is a lengthy process, and it is important to keep user interaction to a manageable level by automating the transformation steps. In this thesis I present an automated technique for transforming a program by changing the data types in that program to ones which are more appropriate for the task. Programs are constructed by proving synthesis theorems in the proofs-as-programs paradigm. Programs are transformed by modifying their synthesis theorems and relating the modified theorem to the original. Proof transformation allows more powerful transformations than program transformation because the proof of the modified theorem yields a program which meets the original specification, but may compute a different function to the original program. Synthesis proofs contain information which is not present in the corresponding program and can be used to aid the transformation process. Type changes are motivated by the presence of certain subexpressions in the synthesised program. A library of possible type changes is maintained, indexed by the motivating subexpressions. I present a new method which extends these type changes from the motivating expressions to cover as much of the program as possible. Once a type change has been chosen, a revised synthesis theorem is constructed automatically. Search is a major problem for program transformation systems. The synthesis theorems which arise after a type change have a particular form. I present an automated proof strategy for synthesis theorems of this form which requires very little search