A Fully-Abstract Model for the pi-calculus

   M.P. Fiore                E. Moggi                 D. Sangiorgi
<mf@dcs.ed.ac.uk>   <moggi@diana.disi.unige.it>   <davide@duick.cma.fr>

                            Synopsis

This paper provides both a fully abstract (domain-theoretic) model for 
the pi-calculus and a universal (set-theoretic) model for the finite 
pi-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 pi-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 
pi-calculus in the set-theoretic model is axiomatically extended to the
whole pi-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.