Session type embedding for practical concurrent/distributed programming

2023 Fiscal Year Annual Research Report

• Project/Area Number: 21K11827
• Research Institution: Gifu University
• Principal Investigator: 今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml

Outline of Annual Research Achievements

研究実績は大まかに次の3つに分けられる．
(1) セッション型，プログラミング言語の型システムとモデル検査の統合．具体的には，従来の，ソフトウェア全体の通信プロトコル設計とその安全性の検証が必要な「トップダウン型」の開発手法ではなく，それらが不要な「ボトムアップ」の手法を確立し，その実装であるkmclibを実装した．その成果に関する論文は， トップレベル会議の1つである TACAS 2022 に採択された．
(2) セッション型の表現能力に関する探究．(2-1) マルチパーティセッション型の混合選択に関する理論的な検討を行った．混合選択は，通信プロトコル参加者が特定の状態において送信と受信の双方を選択できる機能であるが，これは実用的に重要である一方でデッドロックフリー性などの信頼性に関する理論的な基礎は未整備である．本研究課題では，その無限のトレースを扱うための理論的基礎を検討した．(2-2) マルチパーティセッション型のプロトコルを文脈自由文法へと拡張し，処理系Session C#に実装した．
(3) これらからの派生的な研究．(3-1) 上述(1)の派生として，プログラミング言語OCamlのアドホック多相に関する拡張を設計し実装した．アドホック多相は単一の関数名に対して，引数型に応じた複数の定義本体を与える多重定義の機能である．これにより，OCamlプログラムにおいて型ベースのディスパッチが可能となり，プログラミングの効率向上が期待できる．(3-2) 上述(2-1)の派生として，高階項書換えシステムの活用を検討した．この際，共同研究者である群馬大学浜名准教授の高階項書換えシステムの処理系SOLの改修に関与した．停止性判定ツールのコンペティションTermComp2022に参加し，入賞した．
また，上記(2),(3-1)の進行中の内容や成果を国内ワークショップ・研究会にて発表した．