Typed mobile ambients in Maude

In H. Cirstea and N. Martí-Oliet, editors, Proceedings of the 6th International Workshop on Rule-Based Programming (RULE 2005), ENTCS 147, pages 135-161. Elsevier, 2006.

Abstract: 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.

  [pdf]

@inproceedings{RosaSeguraVerdejo05,
	Author = {Fernando Rosa-Velardo and Clara Segura and Alberto Verdejo},
	Booktitle = {Proceedings of the 6th International Workshop on Rule-Based Programming (RULE 2005)},
	Editor = {H. Cirstea and N. Mart{\'\i}-Oliet},
	Pages = {135--161},
	Publisher = {Elsevier},
	Series = {Electronic Notes in Theoretical Computer Science},
	Title = {Typed Mobile Ambients in {Maude}},
	Volume = {147},
	Year = {2006}}