研究課題/領域番号 |
21K11827
|
研究種目 |
基盤研究(C)
|
配分区分 | 基金 |
応募区分 | 一般 |
審査区分 |
小区分60050:ソフトウェア関連
|
研究機関 | 岐阜大学 |
研究代表者 |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
研究期間 (年度) |
2021-04-01 – 2024-03-31
|
研究課題ステータス |
中途終了 (2022年度)
|
配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2024年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2023年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円)
2022年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2021年度: 910千円 (直接経費: 700千円、間接経費: 210千円)
|
キーワード | 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml / モデル検査 / 並行プログラミング / 型システム / 分散プログラミング |
研究開始時の研究の概要 |
プログラミング言語の「型」は,整数や文字列などの「データ」を分類し間違いを事前に検出するための仕組みです.これに類似する枠組みとして,例えばインターネットで用いられる通信ポートは,HTTP や SMTP といった通信プロトコルで分類されています.セッション型はこの「通信ポート」のプロトコルを表す「型」であり,プログラムにおけるデッドロックや競合条件などの通信記述の誤りを事前に検出できます. 本研究は,セッション型をプログラミング言語において活用する軽量な方法を理論と実装の両面で開発します.これにより,多くの人が高信頼な並行分散ソフトウェアを手軽に構築できるようになることを目指します.
|
研究実績の概要 |
今年度の実績は次の3点である: (1) 国際学会およびワークショップにおける発表.昨年度までの成果を,(1a) トップレベル国際会議TACAS 2022および,(1b) セッション型に関する発表が多く行われる国際ワークショップPLACES 2022で発表した. (2) セッション型のグローバル型に関する意味論を整理し,プログラミング言語 Coq で一部を定式化し国内研究会で発表した.これまでの意味論では扱えなかった,一部のノードのみが参加するループを含むプロトコルを扱えることが特徴であり,本研究が目指すより実用的な枠組みのための基礎理論を試行的に確立できた.論理的基盤として,トレース意味論の定式化にDagninoらの有界な余帰納法を用いた. (3) 本研究から派生して生まれた,プログラミング言語OCamlのアドホック多相に関する拡張について国内研究会で発表した(学生との共著).
|
現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
トップレベル国際会議での発表を達成したことに加え,これまで未着手だったセッション型の意味論に関する理論研究に着手し,Coqによる理論の形式化が進展したことから,おおむね順調に進展していると判断した.(本分野では国際会議論文が雑誌論文と同等かそれ以上の評価を受ける)
|
今後の研究の推進方策 |
本年度は,昨年度に引き続き (1) トップダウン方式のセッション型における理論面の基礎付けを推進する. さらに,実用面では現在進めている (2) プログラミング言語Pythonをベースとしたコレオグラフィプログラミング言語のプロトタイプを完成させ,学会発表を行う. さらに,(3) 産業界の協力者と連携し,これまでに実装した OCaml向けマルチパーティセッション型の実装を実用に向けて整備する.
|