Proofs by structural induction using partial evaluation
Julia L. Lawall · 1993
In this paper we show how partial evaluation can be used in developing proofs about program transformations. Partial evaluation is particularly appropriate for this task because it distinguishes between static and dynamic data. As a realistic example of this technique we prove a theorem arising in our earlier study of the CPS transformation. Our approach requires a partial evaluator that supports the following features: resugaring, partially-static structures, higher-order functions, polyvariance, and filters. In particular, we use Consel's partial evaluator Schism.