Categorical Semantics and Logical Interpretation of the Pi-Calculus

2021 Fiscal Year Final Research Report

• Project/Area Number: 19K20211
• Research Category: Grant-in-Aid for Early-Career Scientists
• Allocation Type: Multi-year Fund
• Review Section: Basic Section 60010:Theory of informatics-related
• Research Institution: Chiba University (2020-2021); The University of Tokyo (2019)
• Principal Investigator: Tsukada Takeshi 千葉大学, 大学院理学研究院, 准教授 (50758951)
• Project Period (FY): 2019-04-01 – 2022-03-31
• Keywords: π計算 / 圏論的意味論 / 計算論的ラムダ計算 / 線形論理

Outline of Final Research Achievements

This research project aims to develop a categorical semantics of the pi-calculus. Concurrent computing is a form of computation in which many computers are executed concurrently and work together to perform a computation, and the pi-calculus is a formal calculus modelling the essence of concurrent computing. Despite the importance of the pi-calculus, which has been widely used in the research of concurrent computing, no categorical semantics has been given for the pi-calculus.
The contributions of this research project can be summarised as follows: (1) we pointed out a fundamental difficulty in developing a categorical model of the conventional pi-calculus, (2) we proposed a variant of the pi-calculus, which avoids the difficulty, and gives a simple categorical semantics for the valiant, and (3) we discuss the relationship between the conventional pi-calculus and our variant.

Free Research Field

プログラム意味論

Academic Significance and Societal Importance of the Research Achievements

ネットワークを介して複数の計算機が協働して働くようなソフトウェアの設計・検証は、重要であるが難しい課題である。専門用語を使って言えば、並行システムの設計・検証である。本研究はこの課題への、プログラミング言語を通じた解決策のための基礎的な研究である。人間の持つプログラムの振る舞いに関する直観に数学的に厳密な背景を与えるものが意味論であるが、これまでは（圏論的）意味論を持つ並行システム（具体的にはπ計算）が存在していなかった。本研究はπ計算にはじめての圏論的意味論を与えるもので、今後の並行システム用プログラミング言語の設計や検証への応用が期待される。