2019 Fiscal Year Research-status Report
Session-typed programming in unreliable communication environment
| Project/Area Number |
17K12662
|
|---|
| Research Institution | Gifu University |
|---|
Principal Investigator |
今井 敬吾 岐阜大学, 工学部, 助教 (70456630)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | セッション型 / 関数型プログラミング / 型システム / メタプログラミング / ステージ計算 / OCaml / モナド |
|---|
| Outline of Annual Research Achievements |
通信プログラムがプロトコルに沿って通信することを、メタプログラミング機構とバイナリーセッション型を組み合わせて検査する手法について研究を行った。この方法は前年までに報告したホスト言語の型を利用した検査手法とは異なり、チャネル使用の線形性の検査のためにパラメタ化モナドのようなホスト言語の複雑な型機能を用いる必要がなく、プログラムを見通しよく記述できる。この研究の成果をまとめた論文は関数型および論理型プログラミング言語に関する高レベル国際会議FLOPS 2020に採録された。
また、前年度に引き続き、マルチパーティセッション型を一般的な静的型付きプログラミング言語で利用可能にするための技法に関する研究を進めた。具体的には、マルチパーティセッション型と同等の通信プロトコルを扱えるように拡張した。さらに理論面では核となる計算体系の形式化を行った。この成果はプログラミング言語研究の高レベル国際会議ECOOP 2020に採録された。実装はOCamlのライブラリocaml-mpstとしてGitHubで公開している。
さらに、実践的なプログラミング言語であるC#におけるバイナリーセッション型の実装について研究を行った。C#の様々な言語機能を活用して、コネクションの切断等でメッセージの到達性が必ずしも保証されない通信環境におけるプログラミング技法を開発した。この報告は、国際ワークショップ12th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES 2020)に採録された。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究はおおむね順調に進展している。「研究実績の概要」に述べた通り、本年度は主要な成果であるマルチパーティセッション型の実装技法が大きく拡張され、さらに理論面の整備が進んだ。これに加えて、メタプログラミングを用いた別種の技法も開発できた。これにより、本研究の目的の一つであるセッション型付きプログラミングの技法が充実したといえる。さらに、もう一つの目標であるメッセージの到達性を保証しない通信環境における手法の確立のため、C#における実践的な技法を基礎づけることができた。
|
| Strategy for Future Research Activity |
最終年度として、これまでに実現した技法を統合して、マルチパーティセッション型をより実践的な場面で用いるための技法を確立する。まず、マルチパーティ計算のプロトコルをメタプログラミング機構を用いて検査する手法を確立する。具体的には、型検査ベースの手法と通信オートマトンベースの手法の両方を検討する。さらに、理論面の整備を進める。これに加えて、C#における実装で得られた知見と、既に知られているセッション切断への対処を組み合わせて、メッセージの到達性を保証しない通信環境における手法を確立する。
|
| Causes of Carryover |
理論面の検討が少し遅れ、それまで予定していた国際会議への投稿がなくなったため。これは、2020年度（あるいは、新型コロナウイルス感染症の対処として期間を延長した場合は、2021年度）の旅費として使用する計画である。
|
Research Products
(9 results)
