Imperative Objects and Mobile Processes

Abstract

An interpretation of Abadi and Cardelli's first-order Imperative Object
Calculus into a typed pi-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 pi-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.