I&C Journal 2002 Journal Article
A Fully Abstract Model for the π-calculus
- M.P. Fiore
- E. Moggi
- D. Sangiorgi
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 nondeterminism as a free construction and by the equational theory of the metalanguage.