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 ongroup 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.

A Mobility Calculus with Local Dependent Types

COPPO, Mario;DEZANI, Mariangiola;GIOVANNETTI, Elio;
2005-01-01

Abstract

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 ongroup 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.
Processes, Terms and Cycles: Steps on the Road to Infinity
Springer Verlag Germany:Tiergartenstrasse 17, D 69121 Heidelberg Germany
3838
404
444
354030911X
9783540309116
Ambient Calculi; Type Systems; Type inference
M. COPPO; F. COZZI; M. DEZANI; E. GIOVANNETTI; R. PUGLIESE
File in questo prodotto:
File Dimensione Formato  
CCDGP05.pdf

Accesso riservato

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 437.11 kB
Formato Adobe PDF
437.11 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/102948
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact