A Higher-Order Distributed Calculus with Name Creation

6 years 6 months ago
A Higher-Order Distributed Calculus with Name Creation
—This paper introduces HOpiPn, the higher-order pi-calculus with passivation and name creation, and develops an equivalence theory for this calculus. Passivation [Schmitt and Stefani] is a language construct that elegantly models higher-order distributed behaviours like failure, migration, or duplication (e.g. when a running process or virtual machine is copied), and name creation consists in generating a fresh name instead of hiding one. Combined with higher-order distribution, name creation leads to different semantics from name hiding, and is closer to implementations of distributed systems. We define for this new calculus a theory of sound and complete environmental bisimulation to prove reduction-closed barbed equivalence and (a reasonable form of) congruence. We furthermore define environmental simulations to prove behavioural approximation, and use these theories to show non-trivial examples of equivalence or approximation. Those examples could not be proven with previous th...
Adrien Piérard, Eijiro Sumii
Added 29 Sep 2012
Updated 29 Sep 2012
Type Journal
Year 2012
Where LICS
Authors Adrien Piérard, Eijiro Sumii
Comments (0)