Proofs by Structural Induction using Partial Evaluation

by Julia Lawall
1992-1993

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.

Proofs by Structural Induction using Partial Evaluation

by Julia Lawall 1992-1993

by Julia Lawall
1992-1993