We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation
and program equivalence that arise when compiling object-oriented languages. Our main result is a direct proof, via a small-step
unloading machine, of the correctness of compilation to a closure-based abstract machine. Our second result is that contextual
equivalence of objects coincides with a form of Mason and Talcott's CIU equivalence; the latter provides a tractable means
of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically
resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of CIU equivalence
for an object-oriented language.