Imperative Objects and Mobile Processes
Josva Kleist, Davide Sangiorgi · 1998
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.