TY - JOUR
T1 - Safe ambients
T2 - Abstract machine and distributed implementation
AU - Giannini, Paola
AU - Sangiorgi, Davide
AU - Valente, Andrea
N1 - Funding Information:
Giannini’s work was partially supported by the IST-2001-33477 DART, and MIUR Cofin’01 NAPOLI projects. Sangiorgi’s work was partially supported by the IST-2001-33100 PROFUNDIS project. Valente’s work was partially supported by the IST-2001-33477 DART, MIUR Cofin’01 NAPOLI, and MIUR Cofin’02 McTati projects. The founding bodies are not responsible for any use that might be made of the results presented here.
PY - 2006/2
Y1 - 2006/2
N2 - The abstract machine PAN for a distributed implementation of an ambient calculus is presented. PAN is different from, and simpler than, previous implementations of ambient-like calculi, mainly because: the underlying calculus is typed Safe Ambients (SA) rather than the untyped Ambient calculus and therefore does not present certain forms of interferences among processes (the grave interferences). In PAN the logical structure of an ambient system and its physical distribution are separated. A translation from SA terms to PAN terms is defined. The correctness of such a translation, which asserts that an SA term and its translation exhibit the same observational behavior, is proved. Moreover, a description of a distributed implementation of the abstract machine in Java is given.
AB - The abstract machine PAN for a distributed implementation of an ambient calculus is presented. PAN is different from, and simpler than, previous implementations of ambient-like calculi, mainly because: the underlying calculus is typed Safe Ambients (SA) rather than the untyped Ambient calculus and therefore does not present certain forms of interferences among processes (the grave interferences). In PAN the logical structure of an ambient system and its physical distribution are separated. A translation from SA terms to PAN terms is defined. The correctness of such a translation, which asserts that an SA term and its translation exhibit the same observational behavior, is proved. Moreover, a description of a distributed implementation of the abstract machine in Java is given.
KW - Abstract machine
KW - Distributed implementation
KW - Proof of correctness
KW - Safe ambients
UR - http://www.scopus.com/inward/record.url?scp=27944459689&partnerID=8YFLogxK
U2 - 10.1016/j.scico.2005.05.002
DO - 10.1016/j.scico.2005.05.002
M3 - Article
SN - 0167-6423
VL - 59
SP - 209
EP - 249
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 3
ER -