TY - GEN

T1 - A higher-order distributed calculus with name creation

AU - Piérard, Adrien

AU - Sumii, Eijiro

PY - 2012

Y1 - 2012

N2 - 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 theories, which were either unsound or incomplete under the presence of process duplication and name restriction, or else required universal quantification over general contexts.

AB - 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 theories, which were either unsound or incomplete under the presence of process duplication and name restriction, or else required universal quantification over general contexts.

KW - Distribution and passivation

KW - Environmental bisimulation

KW - Higher-order pi-calculus

KW - Name restriction and creation

KW - Process equivalence

UR - http://www.scopus.com/inward/record.url?scp=84867175334&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84867175334&partnerID=8YFLogxK

U2 - 10.1109/LICS.2012.63

DO - 10.1109/LICS.2012.63

M3 - Conference contribution

AN - SCOPUS:84867175334

SN - 9780769547695

T3 - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

SP - 531

EP - 540

BT - Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

T2 - 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012

Y2 - 25 June 2012 through 28 June 2012

ER -