A higher-order distributed calculus with name creation

Adrien Piérard, Eijiro Sumii

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012
Pages531-540
Number of pages10
DOIs
Publication statusPublished - 2012
Event2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012 - Dubrovnik, Croatia
Duration: 2012 Jun 252012 Jun 28

Publication series

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

Other

Other2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012
CountryCroatia
CityDubrovnik
Period12/6/2512/6/28

Keywords

  • Distribution and passivation
  • Environmental bisimulation
  • Higher-order pi-calculus
  • Name restriction and creation
  • Process equivalence

ASJC Scopus subject areas

  • Computer Science (miscellaneous)
  • Logic

Fingerprint Dive into the research topics of 'A higher-order distributed calculus with name creation'. Together they form a unique fingerprint.

Cite this