2017年4月 - 2021年3月
メッセージの到達性を保証しない通信環境におけるセッション型付きプログラミング
日本学術振興会 科学研究費助成事業 若手研究(B)
- 課題番号
- 17K12662
- 担当区分
- 研究代表者
- 配分額
-
- (総額)
- 4,030,000円
- (直接経費)
- 3,100,000円
- (間接経費)
- 930,000円
マルチパーティセッション型を一般的な静的型付きプログラミング言語で利用可能にするための技法を考案し、OCaml言語において実装した。本技法は、デッドロックフリー性の核となるグローバル型の整合性を、ホスト言語の型検査機構によって検査する。これにより、型検査に成功した(コンパイルに成功した)並行分散プログラムは、デッドロックなしで動作することが保証される。
従来、マルチパーティセッション型は外部ツールからのコード生成によって実現されており、拡張性・柔軟性に乏しかったが、本技法により、マルチパーティセッション型が静的型付きプログラミング言語のライブラリの形で利用可能になる。これによりデッドロックがないプログラムを容易に効率よく実装できるようになるため、並行分散システムの信頼性向上が期待できる。本研究は次年度において国際会議に投稿・発表する。
さらに、昨年度に国際会議で発表した OCaml におけるバイナリーセッション型の実装 session-ocaml を拡張し、論文誌 Science of Computer Programming に extended version として投稿し、採択された。この拡張は、線形型システムを OCaml 上で模倣する枠組みの上にバイナリーセッション型を実装するものであり、線形型を用いた他のプログラミング言語との親和性が高い。
さらに、本研究の副産物的な結果として、パラメタ化モナドと表層構文の工夫により線形型プログラミングを可能にする枠組みを提案した。その実装である LinOCaml は GitHub 上で公開されている。この枠組みにより、リストや木といった構造をもつ線形型付きのデータを扱うことが可能になった。この結果は論文誌 Journal of Information Processing に採択された。
従来、マルチパーティセッション型は外部ツールからのコード生成によって実現されており、拡張性・柔軟性に乏しかったが、本技法により、マルチパーティセッション型が静的型付きプログラミング言語のライブラリの形で利用可能になる。これによりデッドロックがないプログラムを容易に効率よく実装できるようになるため、並行分散システムの信頼性向上が期待できる。本研究は次年度において国際会議に投稿・発表する。
さらに、昨年度に国際会議で発表した OCaml におけるバイナリーセッション型の実装 session-ocaml を拡張し、論文誌 Science of Computer Programming に extended version として投稿し、採択された。この拡張は、線形型システムを OCaml 上で模倣する枠組みの上にバイナリーセッション型を実装するものであり、線形型を用いた他のプログラミング言語との親和性が高い。
さらに、本研究の副産物的な結果として、パラメタ化モナドと表層構文の工夫により線形型プログラミングを可能にする枠組みを提案した。その実装である LinOCaml は GitHub 上で公開されている。この枠組みにより、リストや木といった構造をもつ線形型付きのデータを扱うことが可能になった。この結果は論文誌 Journal of Information Processing に採択された。
- リンク情報
-
- 論文
- Multiparty Session Programming with Global Protocol Combinators
- 論文
- Fluent Session Programming in C#
- 論文
- Lightweight linearly-typed programming with lenses and monads
- 論文
- Towards Bidirectional Synchronization between Communicating Processes and Session Types
- 論文
- Session-ocaml: a Session-based Library with Polarities and Lenses (extended version)
- 論文
- Session-ocaml: A session-based library with polarities and lenses
- 講演・口頭発表等
- A Preliminary Study on Locally Concurrent Multiparty Session Types
- 講演・口頭発表等
- Global Protocol Combinators: static structural multiparty sessions over simply-typed channels
- 講演・口頭発表等
- Session Type Implementations in Functional Programming Languages