2017 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 |
セッション型（バイナリーセッション型）をプログラミング言語 OCaml で利用可能にするライブラリ session-ocaml を開発した 。国際学会 COORDINATION 2017 で発表し、さらにこれを改訂した論文の投稿に招待され、現在投稿中である。ソースコードはオープンソースソフトウェアとしてウェブサイトで公開している。
セッション型は、通信主体（計算機）の間の通信の流れ（セッション）を表現する型であり、プログラムが通信プロトコルに沿って書かれていることを静的に（プログラムを実行することなく、コンパイル時に）確認できる。セッション型のプログラミング言語への導入により、高い信頼性をもつ通信ソフトウェアを効率よく構築できるようになる。
しかしセッション型は「線形性」をもつため、OCaml を含む既存のプログラミング言語への導入が難しいと考えられていた。実際、セッション型をライブラリの形でプログラミング言語に導入する際は線形性の検査を抜きにして行われることが多い。
我々は、関数型プログラミングにおけるパラメタ化モナドと双方向プログラミングの文脈で知られるレンズを融合することにより、OCaml でセッション型を利用可能にした。この手法は従来のHaskellにおける型クラスや Rust におけるアフィン型を利用したセッション型実装と比較して、静的型付きの関数型プログラミング言語全般に適用可能であるという利点がある。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究の進展により、(2)セッション型システムのプログラミング言語処理系への導入が予定より早く達成できた(国際学会に提出した論文も受理され、さらに、英文一報(投稿中)の論文がある)。このほか、本年度の外国旅費で訪問した吉田教授らのグループの助言により、30年以降に実現予定だったマルチパーティセッション型も一部の実装が完了している(平成30年度中に論文投稿予定)。一方、メッセージの到達性に関する理論は現在検討中であり、計画どおり来年度に継続して取り組む。
|
| Strategy for Future Research Activity |
平成30年度は、メッセージの到達性を考慮したπ計算の理論について引き続き検討するとともに、マルチパーティセッション型の実装に関する論文を投稿する。
|
| Causes of Carryover |
研究の進展により次年度の前倒し申請を行った。これは、一部は PIC マイクロコンピュータや ZigBee といった物品を購入予定であったためだが、組込みシステムに詳しい方の助言により、既に購入していた Raspberry Pi での実装でも計画が達成可能であることがわかった。元々、翌年度分として使用予定の金額であったため、使用計画については特段の変更はない。
|
