Imperative objects as mobile processes

An interpretation of Abadi and Cardelliʹs first-order Imperative ς-calculus into a typed π-calculus is presented. The interpretation validates the subtyping relation and the typing judgments of the ς-calculus, and is computationally adequate. The proof of computational adequacy makes use of (a π-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 ς-calculus, and to prove properties about them, within a unified framework.