PolyA: A Generic Polymorphic Type System for Ambient Calculi.
Joe Wells
Abstract
Previous type systems for mobility calculi (the original Mobile
Ambients, its variants and descendants, e.g., Boxed Ambients and
Safe Ambients, and other related systems) offer little support for
generic mobile agents. Previous systems either do not handle
communication at all or globally assign fixed communication types to
ambient names that do not change as an ambient moves around or
interacts with other ambients. This makes it hard to type generic
mobile agents such as a messenger ambient that uses communication
primitives to collect a message of non-predetermined type and
deliver it to a non-predetermined destination.
In contrast, instead of assigning communication types to ambient
names, our new type system PolyA assigns a type to each process P
that gives upper bounds on (1) the possible ambient nesting shapes
of any process P' to which P can evolve, (2) the values that may be
communicated at each location, and (3) the capabilities that can be
used at each location. Because PolyA can type generic mobile
agents, we believe PolyA is the first type system for an ambient
calculus that provides true type polymorphism. We will demonstrate
an implementation of type inference for PolyA for ambient calculi
such as Mobile Ambients, Safe Ambients, Boxed Ambients,
etc. (requests from the audience for specific ambient calculi
variants are welcome!). We have proven principal typings for a
particular restriction of PolyA.