• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2023 年度 実績報告書

セッション型の埋め込みに基づく実用的な並行分散計算

研究課題

研究課題/領域番号 21K11827
研究機関岐阜大学

研究代表者

今井 敬吾  岐阜大学, 工学部, 助教 (70456630)

研究期間 (年度) 2021-04-01 – 2024-03-31
キーワード並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml
研究実績の概要

研究実績は大まかに次の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)の進行中の内容や成果を国内ワークショップ・研究会にて発表した.

URL: 

公開日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi