Maude has revealed 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'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 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 provide two different (equivalent) ways of implementing such non-determinism in the rules.
Technical report: TR-tmam.pdf
Maude code:
We would appreciate any comment ({fernandorosa, csegura, alberto} [at] sip . ucm . es).
Thanks.