Abstract:
An interpretation of Abadi and Cardelli's first-order
Imperative Object Calculus into a typed 
-calculus is presented. The
interpretation validates the subtyping relation and the typing judgements of
the Object Calculus, and is computationally adequate. The proof of
computational adequacy makes use of (a -calculus version) of ready
simulation, and of a factorisation of the interpretation into a
functional part and a very simple imperative part. The interpretation can be
used to compare and contrast the Imperative and the Functional Object
Calculi, and to prove properties about them, within a unified
framework
Available as PostScript, PDF, DVI.