中文摘要：

证明互模拟同余通常冗长且易出错．双代数为解决该问题提供统一的框架：若行为函子保持弱回拉，共代数范畴到基范畴的忘却函子有右伴函子，则最大共代数互模拟同余．但已有双代数理论建模类型化π演算存在以下困难：行为函子不保持弱回拉，进程互模拟与共代数互模拟不一致．为解决以上两个问题，用稠密拓扑导出布尔范畴作为语义范畴，令行为函子保持弱回拉；定义一类行为函子，使最大进程互模拟与最大共代数互模拟一致，而迟语义和早语义对应的行为函子属于该类函子．进而给出π演算最大进程互模拟同余的双代数模型，为进一步应用双代数框架对其他复杂演算建模奠定了理论基础．

英文摘要：

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 hialgebraic 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.