Type Assignement for Mobile Objects

We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for object-oriented sequential programming. For the sake of concreteness, and because of practical relevance, we consider objects using message exchange to implement method invocation and overriding. The main contribution of the paper is an intersection type assignment system, obtained by a combination of systems introduced for the Calculus of Mobile Ambients and for the &-calculus. We exploit in the mobility framework a typical feature of the intersection type discipline for object calculi, namely late typing of self. The proposed system is then checked against standard properties of related systems, establishing type invariance and a completeness theorem.