Imperative Objects and Mobile Processes

Josva Kleist
Davide Sangiorgi

December 1998


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


Last modified: 2003-06-08 by webmaster.