• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Categorical Semantics and Logical Interpretation of the Pi-Calculus

Research Project

Project/Area Number 19K20211
Research Category

Grant-in-Aid for Early-Career Scientists

Allocation TypeMulti-year Fund
Review Section Basic Section 60010:Theory of informatics-related
Research InstitutionChiba University (2020-2021)
The University of Tokyo (2019)

Principal Investigator

Tsukada Takeshi  千葉大学, 大学院理学研究院, 准教授 (50758951)

Project Period (FY) 2019-04-01 – 2022-03-31
Project Status Completed (Fiscal Year 2021)
Budget Amount *help
¥3,120,000 (Direct Cost: ¥2,400,000、Indirect Cost: ¥720,000)
Fiscal Year 2021: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2020: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Keywordsπ計算 / 圏論的意味論 / 計算論的ラムダ計算 / 線形論理 / η則 / 計算効果 / 並行計算 / Freyd圏
Outline of Research at the Start

並行計算とは、複数のプロセスが相互作用しながら同時に実行される計算である。例えば、ネットワークを介したサーバとクライアントの協働や、複数のコアやプロセッサを持つ計算機でのタスクの実行などが挙げられる。並行計算にはデッドロック・競合状態や命令実行順序の非決定性などの厄介な問題があり、逐次処理に比べて、正しい設計を行うことや正しさの検証が特別難しい。こうした課題へのアプローチとして、本研究では、並行計算の本質的な部分を抽象化した筋の良い計算モデルを与え、これを用いて設計や検証を行うことを狙いとする。本研究の特徴は、道具として圏論的意味論や論理学の研究の蓄積を知見を利用することにある。

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.

Academic Significance and Societal Importance of the Research Achievements

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

Report

(4 results)
  • 2021 Annual Research Report   Final Research Report ( PDF )
  • 2020 Research-status Report
  • 2019 Research-status Report
  • Research Products

    (2 results)

All 2021 2019

All Journal Article (2 results) (of which Peer Reviewed: 2 results,  Open Access: 2 results)

  • [Journal Article] Output Without Delay: A π-Calculus Compatible with Categorical Semantics2021

    • Author(s)
      Ken Sakayori, Takeshi Tsukada
    • Journal Title

      Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction

      Volume: 195

    • Related Report
      2021 Annual Research Report
    • Peer Reviewed / Open Access
  • [Journal Article] A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus2019

    • Author(s)
      Sakayori Ken、Tsukada Takeshi
    • Journal Title

      Proceedings of the 28th European Symposium on Programming

      Volume: 0 Pages: 640-667

    • DOI

      10.1007/978-3-030-17184-1_23

    • ISBN
      9783030171834, 9783030171841
    • Related Report
      2019 Research-status Report
    • Peer Reviewed / Open Access

URL: 

Published: 2019-04-18   Modified: 2023-01-30  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi