| 研究課題/領域番号 |
21K11827
|
|---|
| 研究機関 | 岐阜大学 |
|---|
研究代表者 |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| 研究期間 (年度) |
2021-04-01 – 2025-03-31
|
| キーワード | 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml / モデル検査 |
|---|
| 研究実績の概要 |
今年度の実績は次の3点である： (1) プログラミング言語の型システムの一つであり，並行ソフトウェアの欠陥を静的に（実行前に）排除するセッション型についてさらなる研究を進めた．これにより，より表現能力が高く，かつ省力化された手法を確立できた．具体的には，従来の，ソフトウェア全体の通信プロトコル設計とその安全性の検証が必要な「トップダウン型」の開発手法ではなく，それらが不要な「ボトムアップ」の手法を確立し，その実装であるkmclibを実装した．この方法は，関数型プログラミング言語の型推論機構とプリプロセッサ，および共同研究者のJulien Lange氏が開発したモデル検査器k-MC checkerを組み合わせたものである．これにより，プログラマは全体のプロトコルを意識することなく，信頼性の高い並行プログラムを開発できる．その成果に関する論文は，トップレベル会議の1つである TACAS 2022 に採択された．(2) この副産物として，OCamlにおけるアドホック多相を実現するためのライブラリ実装手法を開発した． (3) これとは別に，コールバック方式によりセッション型付きのプログラムを開発する際の，OCamlの多相性の活用に関するアイデアの発表提案が国際ワークショップPLACES 2022に採択された．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
セッション型を現実のプログラミング言語において少ない労力で活用するための新たな手法を確立することができた．この成果がトップレベル会議に採択されたことから研究コミュニティから一定の評価が得られ，また注目が得られたと判断する．このため，おおむね順調に進展していると判断した．
|
| 今後の研究の推進方策 |
当初の計画で想定していた，(1) トップダウン方式のセッション型における理論面の基礎付け (2) セッション型の産業応用について，2022年度で推進する．(1) は2021年度における基礎調査に基づき理論的な枠組みを確立し，基本的な定理の証明を試みる．(2)は産業界の協力者と連携し，具体的なアプリケーションに対して，我々が開発したOCaml言語のセッション型実装を適用する．
|
| 次年度使用額が生じた理由 |
新型コロナウイルス感染症の蔓延のため国内外の移動が制限され，想定された旅費の支出がなかったため．
|
