PRL Seminars

We show how partial evaluation can be used in developing proofs by structural induction about program transformations. Partial evaluation is particularly appropriate for this task because it distinguishes between static and dynamic data.

This approach requires a partial evaluator that supports the following features: resugaring; partially-static structures; higher-order functions; polyvariance; and filters (we use Consel's partial evaluator, Schism).

As a realistic example of this technique we prove a theorem arising in our earlier study of the CPS transformation.