Torben Amtoft and J. B. Wells
Mobile
processes with dependent communication types and singleton types for names
and capabilities
Technical Report 2002-3, Kansas State University, Department of
Computing and Information Sciences, December 2002
There are many calculi for reasoning about
concurrent communicating processes which have
locations and are mobile. Examples include the
original Ambient Calculus and its many variants, the
Seal Calculus, the MR-calculus, the M-calculus,
etc. It is desirable to use such calculi to describe
the behavior of mobile agents. It seems reasonable
that mobile agents should be able to follow
non-predetermined paths and to carry
non-predetermined types of data from location to
location, collecting and delivering this data using
communication primitives. Previous type systems for
ambient calculi make this difficult or impossible to
express, because these systems (if they handle
communication at all) have always globally mapped
each ambient name to a type governing the type of
values that can be communicated locally or with
adjacent locations, and this type can not depend on
where the ambient has traveled. We present a
new type system where there are no global
assignments of types to ambient names. Instead, the
type of an ambient process P not only indicates
what can be locally communicated but also gives an
upper bound on the possible ambient nesting shapes
of any process P' to which P can evolve, as well
as the possible capabilities and names that can be
exhibited or communicated at each location. Because
these shapes can depend on which capabilities and
names are actually communicated, the types support
this with explicit dependencies on
communication. This system is thus the first type
system for an ambient calculus which provides type
polymorphism of the kind that is usually present in
polymorphic type systems for the
lambda-calculus.
[ bib |
.html |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43