Correctness of on-line partial evaluation for a Pascal-like language

An on-line partial evaluator for an imperative language is formally defined and proven to be correct. As far as we know, this is the first correctness proof of an on-line partial evaluator. The proof consists of several lemmata showing the correctness of partial evaluation of expression and the invariance of certain properties of the environments under partial/residual and total evaluation. The language the partial evaluator is based on contains functions as well as procedures with value, result, and reference parameters and side-effects.