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 as 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. |
Papers
