TY - JOUR AU - Gordon, Andrew D. AU - Hankin, Paul D. AU - Lassen, Søren B. PY - 1998/12/15 Y2 - 2024/03/28 TI - Compilation and Equivalence of Imperative Objects (Revised Report) JF - BRICS Report Series JA - BRICS VL - 5 IS - 55 SE - Articles DO - 10.7146/brics.v5i55.19500 UR - https://tidsskrift.dk/brics/article/view/19500 SP - AB - 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. ER -