Logo del repository
  1. Home
 
Opzioni

Ambient Calculus and its Logic in the Calculus of Inductive Constructions

SCAGNETTO, Ivan
•
MICULAN, Marino
2002
  • conference object

Periodico
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE
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.
DOI
10.1016/S1571-0661(04)80507-3
Archivio
http://hdl.handle.net/11390/677720
info:eu-repo/semantics/altIdentifier/scopus/2-s2.0-19044374305
http://www.sciencedirect.com/science/article/pii/S1571066104805073
Diritti
closed access
Soggetti
  • Ambient Calculu

  • Inductive contruction...

  • Logical Framework (LF...

  • Theory of Contexts

Scopus© citazioni
7
Data di acquisizione
Jun 14, 2022
Vedi dettagli
Visualizzazioni
1
Data di acquisizione
Apr 19, 2024
Vedi dettagli
google-scholar
Get Involved!
  • Source Code
  • Documentation
  • Slack Channel
Make it your own

DSpace-CRIS can be extensively configured to meet your needs. Decide which information need to be collected and available with fine-grained security. Start updating the theme to match your nstitution's web identity.

Need professional help?

The original creators of DSpace-CRIS at 4Science can take your project to the next level, get in touch!

Realizzato con Software DSpace-CRIS - Estensione mantenuta e ottimizzata da 4Science

  • Impostazioni dei cookie
  • Informativa sulla privacy
  • Accordo con l'utente finale
  • Invia il tuo Feedback