Paper: Bisimulation in Name-Passing Calculi without Matching (at LICS 1998)

Authors: Michele Boreale Davide Sangiorgi

Abstract

We study barbed equivalence in name-passing languages where there is no matching construct for testing equality between names. We concentrate on the π-calculus with capability types and subtypes, of which the untyped π-calculus without matching is a special case. We give a coinductive characterisation of typed barbed equivalence, and present "bisimulation up-to" techniques to enhance the resulting coinductive proof method. We then use these techniques to prove some process equalities that fail in the ordinary π-calculus

BibTeX

  @InProceedings{BorealeSangiorgi-BisimulationinNameP,
    author = 	 {Michele Boreale and Davide Sangiorgi},
    title = 	 {Bisimulation in Name-Passing Calculi without Matching},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {165--175},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }