2022 Fiscal Year Research-status Report
Session type embedding for practical concurrent/distributed programming
| 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) 国際学会およびワークショップにおける発表．昨年度までの成果を，(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向けマルチパーティセッション型の実装を実用に向けて整備する．
|
| Causes of Carryover |
新型コロナウイルス感染症の蔓延のため国内外の移動が制限され，想定された旅費の支出がなかったため．
|
