Logic in Computer Science (LICS 1999)

Paper: Towards a Theory of Bisimulation for Local Names (at LICS 1999)

Authors: Alan Jeffrey Julian Rathke

Abstract

Pitts and Stark have proposed the n-calculus as a language for investigating the interaction of unique name generation and higher-order functions. They developed a sound model based on logical relations, but left completeness as an open problem. In this paper, we develop a complete model based on bisimulation for a labelled transition system semantics. We show that bisimulation is complete, but not sound, for the n-calculus. We also show that by adding assignment to the n-calculus, bisimulation becomes sound and complete. The analysis used to obtain this result illuminates the difficulties involved in finding fully abstract models for n-calculus proper.

BibTeX

  @InProceedings{JeffreyRathke-TowardsaTheoryofBis,
    author = 	 {Alan Jeffrey and Julian Rathke},
    title = 	 {Towards a Theory of Bisimulation for Local Names},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1999},
    year =	 1999,
    editor =	 {Giuseppe Longo},
    month =	 {July}, 
    pages =      {56--66},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }