Lics

IEEE Symposium on Logic in Computer Science

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

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 Symposium on Logic in Computer Science (LICS 1996)},
 year =	 {1996},
 month =	 {July}, 
 pages = {43--54},
 location = {New Brunswick, NJ, USA}, 
 publisher =	 {IEEE Computer Society Press}
 }