We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for 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 contribution of the paper is a type assignment system, obtained by combination of systems for MA and for the Sigma-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 a completeness theorems.
Type Assignment for Mobile Objects
DE' LIGUORO, Ugo
2004-01-01
Abstract
We address the problem of formal reasoning about mobile code. We consider an Ambient Calculus, where process syntax includes constructs for 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 contribution of the paper is a type assignment system, obtained by combination of systems for MA and for the Sigma-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 a completeness theorems.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
