Research on "Formal Methods in Computing"

Type Assignement for Mobile Objects

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.

[pdf] ( © Elsevier )

BIBTEX.

@inproceedings{BarbaneradeLiguoro:COMETA-03,
   author    = {Franco Barbanera, Ugo {de' Liguoro}},
   title     = {{Type Assignement for Mobile Objects}},
   booktitle = {{COMETA'03}},
   year      = {2004},
   publisher = {Elsevier},
   series    = {ENTCS 104C}

}