Bialgebraic Semantics of the Typed π-Calculus

Proofs of bisimilarity being congruence in process calculi are lengthy and error-prone. The bialgebraic semantic provides a uniform framework to solve this problem. If the behavior functor over the semantic category preserves weak pullbacks and the forgetful functor from the category of coalgebras to the underlying semantic category has right adjoint, then the greatest coalgebraic bisimulation is congruence. When applying the bialgebraic framework to model the typed π-calculus, two problems arise: the behavior functors do not preserve weak pullbacks, and process bisimulations do not coincide with coalgebraic bisimulations. Solutions to the above two problems are proposed. For the first problem, the dense topology over the category of closed contexts is used to derive a boolean sheaf subcategory of the semantic category, so that the behavior functors, resulting from being restricted into such Boolean subcategory, preserve weak pullbacks. For the second problem, a specific class of functors over the Boolean sheaf subcategory, which includes the behavior functors for earlylate semantics, is defined. That process bisimilarity induced by these functors is the greatest coalgebraic bisimulation is proved. The existing bialgebraic framework is improved by using the above two techniques, and an appropriate bialgebraic model for the typed π-calculus is given. The corresponding bialgebraic semantic is fully abstract, and process bisimilarity is congruence. The methods described have paved the way for modelling more complex calculi in the bialgebraic framework.