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

2015 年度 実施状況報告書

相互作用の幾何の確率拡張――圏論的意味論からビッグデータへ

研究課題

研究課題/領域番号 15K11984
研究機関東京大学

研究代表者

蓮尾 一郎  東京大学, 情報理工学(系)研究科, 准教授 (60456762)

研究分担者 星野 直彦  京都大学, 数理解析研究所, 助教 (20611883)
研究期間 (年度) 2015-04-01 – 2018-03-31
キーワードプログラミング言語理論 / 表示的意味論 / 操作的意味論 / 抽象機械 / 高階計算 / 確率的プログラミング / 圏論 / 線形論理
研究実績の概要

2015年度においては理論面での大きな進展があり,この成果がプログラミング言語分野のトップ国際会議に採択され発表した [室屋・星野・蓮尾,POPL’16].この論文では,本研究の基盤となった [星野・室屋・蓮尾,CSL-LICS’14] の枠組みに再帰計算を導入し,Plotkin-Power 流の計算副作用付き操作的意味論との対応(妥当性 adequacy)を示した.この成果は,本研究の基礎となる GoI 抽象機械の(数学的に定義された)振る舞いがプログラミング言語的見地から自然・妥当なものであることを示すものであり,今後の研究の理論的基盤をさらに強化する結果として重要である.
上記とは別の理論的進展として,(確率的分岐などの)さまざまな「分岐」を持つプログラム及びシステムの解析・検証手法として,クライスリ圏の中の余代数の理論の研究を発展させた.たとえば [卜部・蓮尾,CALCO’15] においては,[蓮尾,CONCUR’06] のクライスリ模倣の概念が,システムの生成する(無限語や無限木などの)無限トレースの包含関係に対しても健全であることを一般的に示した.この理論の次の大きな一歩として,Buechi 及び parity 受理条件を持つシステムに対しての研究も行った.
確率的プログラム処理系の専用ハードウェア実装の目標に対しては,前年度得られたコンパイラ及びシミュレータを洗練し,web インターフェイスを作成して公開した(http://koko-m.github.io/TtT/).専用ハードウェア実装の基礎となるであろうこのツールについては,上記 POPL 論文の発表時にも言及し,多数の聴衆の興味を集めた.
確率的プログラムの一般静的解析アルゴリズムの目標に対しては,GoI 抽象機械を行列として表現することによってさまざまな問題を線形計画法に帰着するというアイデアを得て,研究を開始した.

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

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

理由

挑戦的目標をかかげた本研究において,当初設定した獲得目標の達成に向け着実にサーベイや理論上の準備的知見,さらにプロトタイプ実装を積み重ねている.理論的研究については特に関連する(GoI や余代数に関する)一般論についてブレイクスルー的成果が生まれており,それら理論的成果の本研究目標への貢献が今後期待される.

今後の研究の推進方策

これまで順調に推移している研究を引き続き継続するとともに,特にハードウェア実装について,豊富な研究開発経験を持つ海外の研究者との協働を模索する(すでに準備的議論を開始している).

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

計画した旅費の額と実際の額の間に誤差が生じた.

次年度使用額の使用計画

物品費または旅費に充当する.

  • 研究成果

    (25件)

すべて 2016 2015 その他

すべて 国際共同研究 (4件) 雑誌論文 (10件) (うち国際共著 4件、 査読あり 9件、 謝辞記載あり 4件、 オープンアクセス 1件) 学会発表 (8件) (うち国際学会 8件、 招待講演 1件) 図書 (1件) 備考 (2件)

  • [国際共同研究] Univ. Bologna/INRIA Sophia Antipolis/hoge/hoge(イタリア)

    • 国名
      イタリア
    • 外国機関名
      Univ. Bologna/INRIA Sophia Antipolis/hoge/hoge
  • [国際共同研究] University of Paris VII/Verimag(フランス)

    • 国名
      フランス
    • 外国機関名
      University of Paris VII/Verimag
  • [国際共同研究] Radboud University(オランダ)

    • 国名
      オランダ
    • 外国機関名
      Radboud University
  • [国際共同研究] University of Southampton/University of Bath(英国)

    • 国名
      英国
    • 外国機関名
      University of Southampton/University of Bath
  • [雑誌論文] Healthiness from Duality2016

    • 著者名/発表者名
      Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
    • 雑誌名

      Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)

      巻: - ページ: 682-691

    • DOI

      10.1145/2933575.2935319

    • 査読あり / 国際共著 / 謝辞記載あり
  • [雑誌論文] Semantics of Higher-Order Quantum Computation via Geometry of Interaction2016

    • 著者名/発表者名
      Ichiro Hasuo and Naohiko Hoshino
    • 雑誌名

      Annals of Pure and Applied Logic

      巻: 未定 ページ: 未定

    • 査読あり / 謝辞記載あり
  • [雑誌論文] Special Issue on Quantum Physics and Logic (QPL 2014)2016

    • 著者名/発表者名
      Ichiro Hasuo and Prakash Panangaden, editors
    • 雑誌名

      New Generation Computing

      巻: 34 ページ: 1-152

    • DOI

      10.1007/s00354-016-0200-7

    • 国際共著
  • [雑誌論文] Lattice-theoretic progress measures and coalgebraic model checking2016

    • 著者名/発表者名
      Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
    • 雑誌名

      Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016

      巻: なし ページ: 718-732

    • DOI

      10.1145/2837614.2837673

    • 査読あり / 国際共著
  • [雑誌論文] Memoryful Geometry of Interaction II: Recursion and Adequacy2016

    • 著者名/発表者名
      Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
    • 雑誌名

      Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016

      巻: なし ページ: 748-760

    • DOI

      10.1145/2837614.2837672

    • 査読あり / 謝辞記載あり
  • [雑誌論文] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis2016

    • 著者名/発表者名
      Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
    • 雑誌名

      Proc. Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016, Lecture Notes in Computer Science

      巻: 9583 ページ: 229-249

    • DOI

      10.1007/978-3-662-49122-5_11

    • 査読あり / 国際共著
  • [雑誌論文] Near-Optimal Scheduling for LTL with Future Discounting2016

    • 著者名/発表者名
      Shota Nakagawa and Ichiro Hasuo
    • 雑誌名

      Proc. Trustworthy Global Computing - 10th International Symposium, TGC 2015, Lecture Notes in Computer Science

      巻: 9533 ページ: 112-130

    • DOI

      10.1007/978-3-319-28766-9_8

    • 査読あり
  • [雑誌論文] Coalgebraic Infinite Traces and Kleisli Simulations2015

    • 著者名/発表者名
      Natsuki Urabe and Ichiro Hasuo
    • 雑誌名

      Proc. 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, LIPIcs

      巻: 35 ページ: 320-335

    • DOI

      10.4230/LIPIcs.CALCO.2015.320

    • 査読あり / オープンアクセス / 謝辞記載あり
  • [雑誌論文] Generic Weakest Precondition Semantics from Monads Enriched with Order2015

    • 著者名/発表者名
      Ichiro Hasuo
    • 雑誌名

      Theoretical Computer Science

      巻: 604 ページ: 2-29

    • DOI

      10.1016/j.tcs.2015.03.047

    • 査読あり
  • [雑誌論文] Time Robustness in MTL and Expressivity in Hybrid System Falsification2015

    • 著者名/発表者名
      Takumi Akazaki and Ichiro Hasuo
    • 雑誌名

      Proc. Computer Aided Verification - 27th International Conference, CAV 2015, Lecture Notes in Computer Science

      巻: 9207 ページ: 356-374

    • DOI

      10.1007/978-3-319-21668-3_21

    • 査読あり
  • [学会発表] Healthiness from Duality2016

    • 著者名/発表者名
      Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
    • 学会等名
      Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016)
    • 発表場所
      New York City, USA
    • 年月日
      2016-07-05 – 2016-07-08
    • 国際学会
  • [学会発表] Coalgebras and Higher-Order Computation: a GoI Approach2016

    • 著者名/発表者名
      Ichiro Hasuo
    • 学会等名
      1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
    • 発表場所
      Porto, Portugal
    • 年月日
      2016-06-22 – 2016-06-26
    • 国際学会 / 招待講演
  • [学会発表] Lattice-theoretic progress measures and coalgebraic model checking2016

    • 著者名/発表者名
      Ichiro Hasuo, Shunsuke Shimizu, and Corina Cirstea
    • 学会等名
      The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
    • 発表場所
      St. Petersburg, Florida, United States
    • 年月日
      2016-01-20 – 2016-01-23
    • 国際学会
  • [学会発表] Memoryful Geometry of Interaction II: Recursion and Adequacy2016

    • 著者名/発表者名
      Koko Muroya, Naohiko Hoshino and Ichiro Hasuo
    • 学会等名
      The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016
    • 発表場所
      St. Petersburg, Florida, United States
    • 年月日
      2016-01-20 – 2016-01-23
    • 国際学会
  • [学会発表] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis2016

    • 著者名/発表者名
      Kengo Kido, Swarat Chaudhuri and Ichiro Hasuo
    • 学会等名
      Verification, Model Checking, and Abstract Interpretation - 17th International Conference, VMCAI 2016
    • 発表場所
      St. Petersburg, Florida, United States
    • 年月日
      2016-01-17 – 2016-01-19
    • 国際学会
  • [学会発表] Near-Optimal Scheduling for LTL with Future Discounting2015

    • 著者名/発表者名
      Shota Nakagawa and Ichiro Hasuo
    • 学会等名
      Trustworthy Global Computing - 10th International Symposium, TGC 2015
    • 発表場所
      Madrid, Spain
    • 年月日
      2015-08-31 – 2015-09-01
    • 国際学会
  • [学会発表] Time Robustness in MTL and Expressivity in Hybrid System Falsification2015

    • 著者名/発表者名
      Takumi Akazaki and Ichiro Hasuo
    • 学会等名
      Computer Aided Verification - 27th International Conference, CAV 2015
    • 発表場所
      San Fransisco, CA, USA
    • 年月日
      2015-07-18 – 2015-07-24
    • 国際学会
  • [学会発表] Coalgebraic Infinite Traces and Kleisli Simulations2015

    • 著者名/発表者名
      Natsuki Urabe and Ichiro Hasuo
    • 学会等名
      6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
    • 発表場所
      Nijmegen, the Netherlands
    • 年月日
      2015-06-24 – 2015-06-26
    • 国際学会
  • [図書] 圏論の歩き方2015

    • 著者名/発表者名
      圏論の歩き方委員会 (編集)
    • 総ページ数
      295
    • 出版者
      日本評論社
  • [備考] 東京大学蓮尾研ウェブページ

    • URL

      http://www-mmm.is.s.u-tokyo.ac.jp/

  • [備考] 研究代表者個人ウェブページ

    • URL

      http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/

URL: 

公開日: 2017-01-06   更新日: 2022-02-03  

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

Powered by NII kakenhi