A Denotational Semantics for the π-Calculus

In his categorical framework, Stark defines a domain-theoretic model for the π-calculus based on functor categories. Despite being a sound abstract model, a more concrete semantics is required if it is to be used as a basis for proving properties about mobile systems. In this paper, we concretize Stark’s denotational model for the π-calculus and provide a full definition of the semantic domains involved. We also include an example of how the model may be approximated in an abstract interpretation analysis.