研究課題
今年度は研究期間の延長により実施が認められた最終年度である．昨年度に，多者間通信の静的型付けの枠組みであるマルチパーティセッション型をOCaml言語の単一の枠組みのみで利用可能にするための技法を確立し，その実装であるOCaml-MPSTを実装した．今年度は，この手法について3点の改良を行った．(1) 通信プロトコルの表現能力を，mixed choiceの機能へと拡張した．これは，ある通信ステップにおけるアクションの選択肢が，送信と受信の双方を含みうるよう修正するものである．これにより，受信のタイムアウト時に送信を行うといった，実用的な通信ソフトウェアの振舞いをコンパイラによって検証できる．(2) 実装面において，通信プロトコルの分岐の記述が煩雑であった問題を，OCamlの型推論器とプリプロセッサを活用する手法を開発することにより修正した． (3) また，通信プロトコルにおけるループの表現に存在した問題を修正した．さらに，これまでの実績についてアカデミアにおける普及活動を行った．具体的には，並行システムの理論と実践に関するワークショップICE2021，および関数型言語のワークショップML2021で発表した．この成果の副産物として，(4) OCamlコンパイラとモデル検査器を組み合わせた新しい手法とその実装Kmclib，および (5) OCamlにおけるアドホック多相を実現するためのライブラリ実装手法を開発した．これらは主に2022年度より開始した提案者の基盤(C)の課題にかかるものであるが，一部は本課題の成果に依っている．(4) はトップレベル会議TACAS 2022に採択された．(5)は国内のプログラミング言語関連の主要ワークショップPPL 2022においてポスター発表し，さらに研究を継続することとなった．
すべて 2022 2021 その他
すべて 国際共同研究 (1件) 雑誌論文 (1件) (うち国際共著 1件、 査読あり 1件、 オープンアクセス 1件) 学会発表 (7件) (うち国際学会 3件) 備考 (2件)
TACAS 2022: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science
巻: 13243 ページ: 379～386
10.1007/978-3-030-99524-9_20
https://github.com/keigoi/ocaml-mpst
https://github.com/keigoi/kmclib
