Mario Coppo, Federico Cozzi, Mariangiola Dezani-Ciancaglini, Elio
Giovannetti, and Rosario Pugliese
A mobility calculus with local and dependent
types
In Festschrift, LNCS 2005
to appear
We introduce an ambient calculus
that combines ambient mobility with process mobility, uses group names
to group ambients with
homologous features, and exploits co-moves and runtime type
checking to implement flexible policies for controlling process
activities. Types rely on group names and, to support dynamicity,
may depend on group variables. Policies can dynamically
change also through installation of co-moves. The compliance with
ambient policies can be checked locally to the ambients and
requires no global assumptions. We prove that the type assignment
system and the operational semantics of the calculus are `sound',
and we define a sound and complete type inference algorithm which,
when applied to terms whose type decorations only express the
desired policies, computes the minimal type annotations required
for their execution. As an application of our calculus, we
present a couple of examples and linger on the setting up of policies for
controlling the activities of the objects involved.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43