Typed Mobile Ambients in Maude

Maude has revealed itself as a powerful tool for implementing different kinds of semantics so that quick prototypes are available for trying examples and proving properties. In this paper we show how to define in Maude two semantics for Cardelli and Gordon's Ambient Calculus. The first one is t...

Full description

Saved in:
Bibliographic Details
Published in:Electronic notes in theoretical computer science 2006-01, Vol.147 (1), p.135-161
Main Authors: Rosa-Velardo, Fernando, Segura, Clara, Verdejo, Alberto
Format: Article
Language:English
Subjects:
Ambient calculus
Maude
operational semantics
type systems
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Maude has revealed itself as a powerful tool for implementing different kinds of semantics so that quick prototypes are available for trying examples and proving properties. In this paper we show how to define in Maude two semantics for Cardelli and Gordon's Ambient Calculus. The first one is the operational (reduction) semantics which requires the definition of Maude strategies in order to avoid infinite loops. The second one is a type system defined by Cardelli and Gordon to avoid communication errors. The correctness of that system was not formally proved. We enrich the operational semantics with error rules and prove that well-typed processes do not produce such errors. The type system is highly non-deterministic. We show here one possible way of implementing such non-determinism in the rules.
ISSN:1571-0661
1571-0661
DOI:10.1016/j.entcs.2005.06.041