Record Details

Compilation and Equivalence of Imperative Objects (Revised Report)

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title Compilation and Equivalence of Imperative Objects (Revised Report)
 
Creator Gordon, Andrew D.
Hankin, Paul D.
Lassen, Søren B.
 
Description We adopt the untyped imperative object calculus of Abadi andCardelli as a minimal setting in which to study problems of compilationand program equivalence that arise when compiling object orientedlanguages. We present both a big-step and a small-stepsubstitution-based operational semantics for the calculus. Our firsttwo 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 CIUequivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used inour prototype compiler, for statically resolving method offsets. This isthe first study of correctness of an object-oriented abstract machine,and of operational equivalence for the imperative object calculus.
 
Publisher Aarhus University
 
Contributor —
 
Date 1998-12-15
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
—
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/19500
10.7146/brics.v5i55.19500
 
Source BRICS Report Series; No 55 (1998): RS-55 Compilation and Equivalence of Imperative Objects (Revised Report)
BRICS Report Series; No 55 (1998): RS-55 Compilation and Equivalence of Imperative Objects (Revised Report)
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/19500/17122
 
Rights Copyright (c) 2014 BRICS Report Series