Previous type systems for mobility calculi 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 examples 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, we present our new type system PolyA. Instead of assigning communication types to ambient names, PolyA assigns a type to each process P that gives upper bounds on the possible ambient nesting shapes of any process P' to which P can evolve, and its available capabilities. Because PolyA can type generic mobile agents, we believe PolyA is the first type system for a mobility calculus that provides type polymorphism comparable in power to polymorphic type systems for the lambda-calculus. A restriction of PolyA has principal typings.

Joint work with Torben Amtoft and Joe Wells.