Imperative objects as mobile processes

An interpretation of Abadi and Cardelli's first-order Imperative S-calculus into a typed pi-calculus is presented. The interpretation validates the subtyping relation and the typing judgments of the zeta-calculus, and is computationally adequate. The proof of computational adequacy makes use of (a pi-calculus version) of ready simulation, and of a factorization of the interpretation into a functional part and a very simple imperative part. The interpretation can be extended to accommodate various type features. The interpretation can be used to compare and contrast the Imperative and the Functional zeta-calculus, and to prove properties about them, within a unified framework. (C) 2002 Elsevier Science B.V. All rights reserved.