• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2019 年度 実施状況報告書

メッセージの到達性を保証しない通信環境におけるセッション型付きプログラミング

研究課題

研究課題/領域番号 17K12662
研究機関岐阜大学

研究代表者

今井 敬吾  岐阜大学, 工学部, 助教 (70456630)

研究期間 (年度) 2017-04-01 – 2021-03-31
キーワードセッション型 / 関数型プログラミング / 型システム / メタプログラミング / ステージ計算 / OCaml / モナド
研究実績の概要

通信プログラムがプロトコルに沿って通信することを、メタプログラミング機構とバイナリーセッション型を組み合わせて検査する手法について研究を行った。この方法は前年までに報告したホスト言語の型を利用した検査手法とは異なり、チャネル使用の線形性の検査のためにパラメタ化モナドのようなホスト言語の複雑な型機能を用いる必要がなく、プログラムを見通しよく記述できる。この研究の成果をまとめた論文は関数型および論理型プログラミング言語に関する高レベル国際会議FLOPS 2020に採録された。
また、前年度に引き続き、マルチパーティセッション型を一般的な静的型付きプログラミング言語で利用可能にするための技法に関する研究を進めた。具体的には、マルチパーティセッション型と同等の通信プロトコルを扱えるように拡張した。さらに理論面では核となる計算体系の形式化を行った。この成果はプログラミング言語研究の高レベル国際会議ECOOP 2020に採録された。実装はOCamlのライブラリocaml-mpstとしてGitHubで公開している。
さらに、実践的なプログラミング言語であるC#におけるバイナリーセッション型の実装について研究を行った。C#の様々な言語機能を活用して、コネクションの切断等でメッセージの到達性が必ずしも保証されない通信環境におけるプログラミング技法を開発した。この報告は、国際ワークショップ12th Workshop on Programming Language Approaches to Concurrency- & Communication-cEntric Software (PLACES 2020)に採録された。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

研究はおおむね順調に進展している。「研究実績の概要」に述べた通り、本年度は主要な成果であるマルチパーティセッション型の実装技法が大きく拡張され、さらに理論面の整備が進んだ。これに加えて、メタプログラミングを用いた別種の技法も開発できた。これにより、本研究の目的の一つであるセッション型付きプログラミングの技法が充実したといえる。さらに、もう一つの目標であるメッセージの到達性を保証しない通信環境における手法の確立のため、C#における実践的な技法を基礎づけることができた。

今後の研究の推進方策

最終年度として、これまでに実現した技法を統合して、マルチパーティセッション型をより実践的な場面で用いるための技法を確立する。まず、マルチパーティ計算のプロトコルをメタプログラミング機構を用いて検査する手法を確立する。具体的には、型検査ベースの手法と通信オートマトンベースの手法の両方を検討する。さらに、理論面の整備を進める。これに加えて、C#における実装で得られた知見と、既に知られているセッション切断への対処を組み合わせて、メッセージの到達性を保証しない通信環境における手法を確立する。

次年度使用額が生じた理由

理論面の検討が少し遅れ、それまで予定していた国際会議への投稿がなくなったため。これは、2020年度(あるいは、新型コロナウイルス感染症の対処として期間を延長した場合は、2021年度)の旅費として使用する計画である。

  • 研究成果

    (9件)

すべて 2020 2019 その他

すべて 国際共同研究 (1件) 雑誌論文 (4件) (うち国際共著 1件、 査読あり 4件、 オープンアクセス 3件) 学会発表 (1件) 備考 (3件)

  • [国際共同研究] Imperial College London/Brunel University London(英国)

    • 国名
      英国
    • 外国機関名
      Imperial College London/Brunel University London
  • [雑誌論文] Fluent Session Programming in C#2020

    • 著者名/発表者名
      Shunsuke Kimura, Keigo Imai
    • 雑誌名

      PLACES 2020: Proceedings of the 12th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, Dublin, Ireland

      巻: 314 ページ: 61-75

    • DOI

      10.4204/EPTCS.314.6

    • 査読あり / オープンアクセス
  • [雑誌論文] Session Types without Sophistry (System Description)2020

    • 著者名/発表者名
      Oleg Kiselyov, Keigo Imai
    • 雑誌名

      15th International Symposium on Functional and Logic Programming (FLOPS 2020)

      巻: - ページ: -

    • 査読あり
  • [雑誌論文] Multiparty Session Programming with Global Protocol Combinators2020

    • 著者名/発表者名
      Keigo Imai, Rumyana Neykova, Nobuko Yoshida, Shoji Yuen
    • 雑誌名

      34th European Conference on Object-Oriented Programming (ECOOP 2020)

      巻: - ページ: -

    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Lightweight Linearly-typed Programming with Lenses and Monads2019

    • 著者名/発表者名
      Keigo Imai, Jacques Garrigue
    • 雑誌名

      Journal of Information Processing

      巻: 27 ページ: 431~444

    • DOI

      10.2197/ipsjjip.27.431

    • 査読あり / オープンアクセス
  • [学会発表] A Preliminary Study on Locally Concurrent Multiparty Session Types2020

    • 著者名/発表者名
      Keigo Imai
    • 学会等名
      第127回プログラミング研究発表会
  • [備考] Session C#

    • URL

      https://github.com/curegit/session-csharp

  • [備考] Session types via Staging

    • URL

      http://okmij.org/ftp/meta-programming/sessions/0README.dr

  • [備考] Multiparty Session Types in OCaml

    • URL

      https://github.com/keigoi/ocaml-mpst

URL: 

公開日: 2021-01-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi