Advertisement
Published in:
2005 | OriginalPaper | Chapter
A Mobility Calculus with Local and Dependent Types
Authors : Mario Coppo, Federico Cozzi, Mariangiola Dezani-Ciancaglini, Elio Giovannetti, Rosario Pugliese
Published in: Processes, Terms and Cycles: Steps on the Road to Infinity
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
We introduce an ambient-based calculus that combines ambient mobility with process mobility, uses group names to collect 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 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 entities involved.