Ivan Scagnetto and Marino Miculan
Ambient calculus and its logic
in the Calculus of Inductive Constructions
In Frank Pfenning, editor, Proc. LFM '02 Elsevier, 2002
The LFM '02 proceedings appears as ENTCS 70(2)
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.
[ bib |
.pdf ]
Back
This file has been generated by
bibtex2html 1.43