On-line and off-line partial evaluation: semantic specifications and correctness proofs

Abstract This paper presents semantic specifications and correctness proofs for both on-line and offline partial evaluation of strict first-order functional programs. To do so, our strategy consists of defining a core semantics as a basis for the specification of three non-standard evaluations: instrumented evaluation, on-line and off-line partial evaluation. We then use the technique of logical relations to prove the correctness of both on-line and off-line partial evaluation semantics. The contributions of this work are as follows: 1. We provide a uniform framework to defining and proving correct both on-line and off-line partial evaluation. 2. This work required a formal specification of on-line partial evaluation with polyvariant specialization. We define criteria for its correctness with respect to an instrumented standard semantics. As a by-product, on-line partial evaluation appears to be based on a fixpoint iteration process, just like binding-time analysis. 3. We show that binding-time analysis, the preprocessing phase of off-line partial evaluation, is an abstraction of on-line partial evaluation. Therefore, its correctness can be proved with respect to on-line partial evaluation, instead of with respect to the standard semantics, as is customarily done. 4. Based on the binding-time analysis, we formally derive the specialization semantics for off-line partial evaluation. This strategy ensures the correctness of the resulting semantics.