Eleventh Annual IEEE Symposium on

Logic in Computer Science (LICS 1996)

Paper: A Fully-Abstract Model for the pi-calculus (Extended Abstract) (at LICS 1996)

Authors: Marcelo .P. Fiore Eugenio Moggi Davide Sangiorgi

Abstract

This paper provides both a fully abstract (domain-theoretic) model for the π-calculus and a universal (set-theoretic) model for the finite π-calculus with respect to strong late bisimulation and congruence. This is done by: considering categorical models, defining a metalanguage for these models, and translating the π-calculus into the metalanguage. A technical novelty of our approach is an abstract proof of full abstraction: The result on full abstraction for the finite π-calculus in the set-theoretic model is axiomatically extended to the whole π-calculus with respect to the domain-theoretic interpretation. In this proof, a central role is played by the description of non-determinism as a free construction and by the equational theory of the metalanguage

BibTeX

  @InProceedings{FioreMoggiSangiorgi-AFullyAbstractModel,
    author = 	 {Marcelo .P. Fiore and Eugenio Moggi and Davide Sangiorgi},
    title = 	 {A Fully-Abstract Model for the pi-calculus (Extended Abstract)},
    booktitle =  {Proceedings of the Eleventh Annual IEEE Symp. on Logic in Computer Science, {LICS} 1996},
    year =	 1996,
    editor =	 {Edmund M. Clarke},
    month =	 {July}, 
    pages =      {43-54},
    location =   {New Brunswick, NJ, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }