@article{Gordon_Hankin_Lassen_1998, title={Compilation and Equivalence of Imperative Objects (Revised Report)}, volume={5}, url={https://tidsskrift.dk/brics/article/view/19500}, DOI={10.7146/brics.v5i55.19500}, abstractNote={We adopt the untyped imperative object calculus of Abadi and<br />Cardelli as a minimal setting in which to study problems of compilation<br />and program equivalence that arise when compiling object oriented<br />languages. We present both a big-step and a small-step<br />substitution-based operational semantics for the calculus. Our first<br />two results are theorems asserting the equivalence of our substitution based semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott’s CIU<br />equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in<br />our prototype compiler, for statically resolving method offsets. This is<br />the first study of correctness of an object-oriented abstract machine,<br />and of operational equivalence for the imperative object calculus.}, number={55}, journal={BRICS Report Series}, author={Gordon, Andrew D. and Hankin, Paul D. and Lassen, Søren B.}, year={1998}, month={Dec.} }