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

• Type: Journal
• Year: 2012
• Where: LICS
• Authors: Adrien Piérard, Eijiro Sumii
• Keywords: Automated Reasoning, Distribution Name, LICS 2012, Passivation, Pi Calculus