Proving the correctness of recursion-based automatic program transformations

Abstract

This paper shows how the Improvement Theorem-a semantic condition for the total correctness of program transformation on higher-order functional programs-has practical value in proving the correctness of automatic techniques, including deforestation and supercompilation. This is aided by a novel formulation (and generalisation) of deforestation-like transformations, which also greatly adds to the modularity of the proof with respect to extensions to both the language and the transformation rules.