Session type embedding for practical concurrent/distributed programming
| Project/Area Number |
21K11827
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60050:Software-related
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| Project Period (FY) |
2021-04-01 – 2024-03-31
|
| Project Status |
Discontinued (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 並行ソフトウェア / 通信プロトコル / セッション型 / 関数型プログラミング言語 / OCaml / モデル検査 / 並行プログラミング / 型システム / 分散プログラミング |
|---|
| Outline of Research at the Start |
プログラミング言語の「型」は，整数や文字列などの「データ」を分類し間違いを事前に検出するための仕組みです．これに類似する枠組みとして，例えばインターネットで用いられる通信ポートは，HTTP や SMTP といった通信プロトコルで分類されています．セッション型はこの「通信ポート」のプロトコルを表す「型」であり，プログラムにおけるデッドロックや競合条件などの通信記述の誤りを事前に検出できます．
本研究は，セッション型をプログラミング言語において活用する軽量な方法を理論と実装の両面で開発します．これにより，多くの人が高信頼な並行分散ソフトウェアを手軽に構築できるようになることを目指します．
|
| Outline of Annual Research Achievements |
今年度の実績は次の3点である:
(1) 国際学会およびワークショップにおける発表．昨年度までの成果を，(1a) トップレベル国際会議TACAS 2022および，(1b) セッション型に関する発表が多く行われる国際ワークショップPLACES 2022で発表した．
(2) セッション型のグローバル型に関する意味論を整理し，プログラミング言語 Coq で一部を定式化し国内研究会で発表した．これまでの意味論では扱えなかった，一部のノードのみが参加するループを含むプロトコルを扱えることが特徴であり，本研究が目指すより実用的な枠組みのための基礎理論を試行的に確立できた．論理的基盤として，トレース意味論の定式化にDagninoらの有界な余帰納法を用いた．
(3) 本研究から派生して生まれた，プログラミング言語OCamlのアドホック多相に関する拡張について国内研究会で発表した（学生との共著）．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
トップレベル国際会議での発表を達成したことに加え，これまで未着手だったセッション型の意味論に関する理論研究に着手し，Coqによる理論の形式化が進展したことから，おおむね順調に進展していると判断した．（本分野では国際会議論文が雑誌論文と同等かそれ以上の評価を受ける）
|
| Strategy for Future Research Activity |
本年度は，昨年度に引き続き (1) トップダウン方式のセッション型における理論面の基礎付けを推進する. さらに，実用面では現在進めている (2) プログラミング言語Pythonをベースとしたコレオグラフィプログラミング言語のプロトタイプを完成させ，学会発表を行う． さらに，(3) 産業界の協力者と連携し，これまでに実装した OCaml向けマルチパーティセッション型の実装を実用に向けて整備する．
|
Report
(2 results)
Research Products
(15 results)
