An interpretation of typed concurrent objects in the blue calculus

Abstract

We propose an interpretation of a typed concurrent calculus of objects based on the imperative object calculus of Abadi and Cardelli. The target of our interpretation is a version of the blue calculus, a variant of the π-calculus that directly contains functions, with record and firstorder types.We show that reductions and type judgments are derivable in a rather simple and natural way, and that our encoding can be extended to recursive and self-types, as well as to synchronization primitives. We also use our encoding to prove some equational laws on objects. © Springer-Verlag Berlin Heidelberg 2002.