Journal article

Publication year: 1999

Pages: 55-73

Journal: Science of Computer Programming

Volume number: 34

Issue number: 1

ISSN: 0167-6423

DOI Link: https://doi.org/10.1016/S0167-6423(98)00015-X

Publisher: Elsevier

Abstract: 
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. (C) 1999 Published by Elsevier Science B.V. All rights reserved.

Harvard Citation style: Meyer, U. (1999) Correctness of on-line partial evaluation for a Pascal-like language, Science of Computer Programming, 34(1), pp. 55-73. https://doi.org/10.1016/S0167-6423(98)00015-X

APA Citation style: Meyer, U. (1999). Correctness of on-line partial evaluation for a Pascal-like language. Science of Computer Programming. 34(1), 55-73. https://doi.org/10.1016/S0167-6423(98)00015-X