The Ambient Calculus has been recently proposed as a model of mobility of agents in a dynamically changing hierarchy of domains. In this paper, we describe the implementation of the theory and metatheory of Ambient Calculus and its modal logic in the Calculus of Inductive Constructions. We take full advantage of Higher-Order Abstract Syntax, using the Theory of Contexts a fundamental tool for developing formally the metatheory of the object system. Among others, we have successfully proved a set of fresh renamings properties, and formalized the connection between the Theory of Contexts and Gabbay-Pitts' "new" quantifier. As a feedback, we introduce a new definition of satisfaction for the Ambients logic and derive some of the properties originally assumed as axioms in the Theory of Contexts. © 2002 Published by Elsevier Science B. V.

Ambient Calculus and its Logic in the Calculus of Inductive Constructions

SCAGNETTO, Ivan;MICULAN, Marino
2002

Abstract

The Ambient Calculus has been recently proposed as a model of mobility of agents in a dynamically changing hierarchy of domains. In this paper, we describe the implementation of the theory and metatheory of Ambient Calculus and its modal logic in the Calculus of Inductive Constructions. We take full advantage of Higher-Order Abstract Syntax, using the Theory of Contexts a fundamental tool for developing formally the metatheory of the object system. Among others, we have successfully proved a set of fresh renamings properties, and formalized the connection between the Theory of Contexts and Gabbay-Pitts' "new" quantifier. As a feedback, we introduce a new definition of satisfaction for the Ambients logic and derive some of the properties originally assumed as axioms in the Theory of Contexts. © 2002 Published by Elsevier Science B. V.
File in questo prodotto:
File Dimensione Formato  
1-s2.0-S1571066104805073-main.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Non pubblico
Dimensione 240.5 kB
Formato Adobe PDF
240.5 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: http://hdl.handle.net/11390/677720
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 7
  • ???jsp.display-item.citation.isi??? ND
social impact