Torben Amtoft, Henning Makholm, and J. B. Wells
PolyA: True type polymorphism for Mobile
Ambients
In IFIP TC1 3rd Int'l Conf. Theoret. Comput. Sci. (TCS
'04), pages 591-604 Kluwer Academic Publishers, 2004
A more detailed predecessor is [42]
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
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
(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 a mobility calculus that
provides type polymorphism comparable in power to
polymorphic type systems for the
lambda-calculus. PolyA is easily
extended to ambient calculus variants. A restriction
of PolyA has principal typings.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43