新パラダイム計算をねじふせる―多様な意味論的手法の合同・発展・応用

• 研究課題/領域番号: 24680001
• 研究種目: 若手研究(A)
• 配分区分: 一部基金
• 研究分野: 情報学基礎
• 研究機関: 東京大学
• 研究代表者: 蓮尾 一郎 東京大学, 情報理工学(系)研究科, 准教授 (60456762)
• 研究期間 (年度): 2012-04-01 – 2016-03-31
• 研究課題ステータス: 完了 (2015年度)
• 配分額: 19,240千円 (直接経費: 14,800千円、間接経費: 4,440千円); 2015年度: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円); 2014年度: 5,070千円 (直接経費: 3,900千円、間接経費: 1,170千円); 2013年度: 4,420千円 (直接経費: 3,400千円、間接経費: 1,020千円); 2012年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
• キーワード: 新パラダイム計算 / 計算の意味論 / プログラミング言語 / 形式検証 / 物理情報システム / 量子計算 / 関数型プログラミング / 圏論 / プログラム理論 / システム検証 / ハイブリッドシステム / 不動点論理 / 応用数学 / 国際研究者交流（フランス） / 国際研究者交流（イタリア） / 国際情報交換（イタリア） / 国際情報交換（オランダ）

研究成果の概要

計算機の応用領域の多様化などに伴いその社会的重要性が急速に増しつつある（物理情報システムや量子計算などの）新パラダイム計算に対して，その数学的本質の理解が計算システムの品質向上に資するという確信のもと，計算機科学における意味論的諸手法を結集・合同してこの応用上の困難に立ち向かうと共に，この新たな応用に牽引される形で意味論研究の理論的発展を行うことを目指した．当初計画に挙げた獲得目標を（より幅広い形で）ほぼ達成すると共に，理論研究ならではの広範な展開，予想しなかったトピック間のつながりの発見に成功した．

研究成果

• [国際共同研究] Univ. Bologna/INRIA Sophia Antipolis(イタリア)
• [国際共同研究] University of Paris VII/Verimag(フランス)
• [国際共同研究] Radboud University(オランダ)
• [国際共同研究] Rice University(米国)
• [国際共同研究] University of Southampton/University of Bath(英国)
• [雑誌論文] Semantics of Higher-Order Quantum Computation via Geometry of Interaction (2016)
  • 著者名/発表者名: Ichiro Hasuo and Naohiko Hoshino
  • 雑誌名: Annals of Pure and Applied Logic 巻: 未定
  • 査読あり / 謝辞記載あり
• [雑誌論文] Healthiness from Duality (2016)
  • 著者名/発表者名: Wataru Hino, Hiroki Kobayashi, Ichiro Hasuo and Bart Jacobs
  • 雑誌名: Proc. Thirty-First Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2016) 巻: なし
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Special Issue on Quantum Physics and Logic (QPL 2014) (2016)
  • 著者名/発表者名: Ichiro Hasuo and Prakash Panangaden, editors
  • 雑誌名: New Generation Computing 巻: 34 号: 1-2 ページ: 1-152
  • DOI: 10.1007/s00354-016-0200-7
  • 国際共著
• [雑誌論文] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: 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 Adequacy (2016)
  • 著者名/発表者名: 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 Analysis (2016)
  • 著者名/発表者名: 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
  • ISBN: 9783662491218, 9783662491225
  • 査読あり / 国際共著 / 謝辞記載あり
• [雑誌論文] Near-Optimal Scheduling for LTL with Future Discounting (2016)
  • 著者名/発表者名: 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
  • ISBN: 9783319287652, 9783319287669
  • 査読あり / 謝辞記載あり
• [雑誌論文] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: 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 Order (2015)
  • 著者名/発表者名: 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 Falsification (2015)
  • 著者名/発表者名: 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
  • ISBN: 9783319216676, 9783319216683
  • 査読あり
• [雑誌論文] Input Synthesis for Sampled Data Systems by Program Logic (2015)
  • 著者名/発表者名: Takumi Akazaki, Ichiro Hasuo, and Kohei Suenaga
  • 雑誌名: Electronic Proceedings in Theoretical Computer Science 巻: 174 ページ: 22-39
  • DOI: 10.4204/eptcs.174.3
  • 査読あり / オープンアクセス / 謝辞記載あり
• [雑誌論文] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 雑誌名: Computer Aided Verification - 27th International Conference, CAV 2015, Proceedings. Lecture Notes in Computer Science 巻: 未定
  • 査読あり / 謝辞記載あり
• [雑誌論文] Measurements in Proof Nets as Higher-Order Quantum Circuits (2014)
  • 著者名/発表者名: Akira Yoshimizu, Ichiro Hasuo, Claudia Faggian, and Ugo Dal Lago
  • 雑誌名: Lecture Notes in Computer Science 巻: 8410 ページ: 371-391
  • DOI: 10.1007/978-3-642-54833-8_20
  • ISBN: 9783642548321, 9783642548338
  • 査読あり / 謝辞記載あり
• [雑誌論文] Generic Weakest Precondition Semantics from Monads Enriched with Order (2014)
  • 著者名/発表者名: Ichiro Hasuo
  • 雑誌名: Lecture Notes in Computer Science 巻: 8446 ページ: 10-32
  • DOI: 10.1007/978-3-662-44124-4_2
  • ISBN: 9783642387081, 9783642387098
  • 謝辞記載あり
• [雑誌論文] The Geometry of Synchronization (2014)
  • 著者名/発表者名: Ugo Dal Lago, Claudia Faggian, Ichiro Hasuo and Akira Yoshimizu
  • 雑誌名: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 巻: なし ページ: 1-10
  • DOI: 10.1145/2603088.2603154
  • 査読あり / 謝辞記載あり
• [雑誌論文] Memoryful Geometry of Interaction: From Coalgebraic Components to Algebraic Effects (2014)
  • 著者名/発表者名: Naohiko Hoshino, Koko Muroya and Ichiro Hasuo
  • 雑誌名: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) 巻: なし ページ: 1-10
  • DOI: 10.1145/2603088.2603124
  • 査読あり / 謝辞記載あり
• [雑誌論文] Generic Forward and Backward Simulations III: Quantitative Simulations by Matrices (2014)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 雑誌名: Lecture Notes in Computer Science 巻: 8704 ページ: 451-466
  • DOI: 10.1007/978-3-662-44584-6_31
  • ISBN: 9783662445839, 9783662445846
  • 査読あり / 謝辞記載あり
• [雑誌論文] Coinductive Predicates and Final Sequences in a Fibration (2013)
  • 著者名/発表者名: Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs
  • 雑誌名: Electronic Notes in Theoretical Computer Science 巻: 298 ページ: 197-214
  • DOI: 10.1016/j.entcs.2013.09.014
  • 査読あり
• [雑誌論文] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals (2013)
  • 著者名/発表者名: Kohei Suenaga, Hiroyoshi Sekine, and
  • 雑誌名: Proc. POPL 巻: 40 ページ: 417-430
  • DOI: 10.1145/2429069.2429120
  • 査読あり
• [雑誌論文] Exercises in Nonstandard Static Analysis of Hybrid Systems (2012)
  • 著者名/発表者名: Ichiro Hasuo and Kohei Suenaga
  • 雑誌名: Proc. Computer Aided Verification - 24th International Conference, Lecture Notes in Computer Science 巻: 7358 ページ: 462-478
  • DOI: 10.1007/978-3-642-31424-7_34
  • ISBN: 9783642314230, 9783642314247
  • 査読あり
• [学会発表] Healthiness from Duality (2016)
  • 著者名/発表者名: 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
  • 国際学会
• [学会発表] Coalgebras and Higher-Order Computation: a GoI Approach (2016)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
  • 発表場所: Porto, Portugal
  • 年月日: 2016-06-22
  • 国際学会 / 招待講演
• [学会発表] Lattice-theoretic progress measures and coalgebraic model checking (2016)
  • 著者名/発表者名: 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
  • 国際学会
• [学会発表] Memoryful Geometry of Interaction II: Recursion and Adequacy (2016)
  • 著者名/発表者名: 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
  • 国際学会
• [学会発表] Abstract Interpretation with Infinitesimals: Towards Scalability in Nonstandard Static Analysis (2016)
  • 著者名/発表者名: 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
  • 国際学会
• [学会発表] Near-Optimal Scheduling for LTL with Future Discounting (2015)
  • 著者名/発表者名: Shota Nakagawa and Ichiro Hasuo
  • 学会等名: Trustworthy Global Computing - 10th International Symposium, TGC 2015
  • 発表場所: Madrid, Spain
  • 年月日: 2015-08-31
  • 国際学会
• [学会発表] Time Robustness in MTL and Expressivity in Hybrid System Falsification (2015)
  • 著者名/発表者名: Takumi Akazaki and Ichiro Hasuo
  • 学会等名: Computer Aided Verification - 27th International Conference, CAV 2015
  • 発表場所: San Fransisco, CA, USA
  • 年月日: 2015-07-18
  • 国際学会
• [学会発表] Coalgebraic Infinite Traces and Kleisli Simulations (2015)
  • 著者名/発表者名: Natsuki Urabe and Ichiro Hasuo
  • 学会等名: 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
  • 発表場所: Nijmegen, the Netherlands
  • 年月日: 2015-06-24
  • 国際学会
• [学会発表] Compiling Effectful Terms to Transducers: Prototype Implementation of Memoryful Geometry of Interaction (2014)
  • 著者名/発表者名: Koko Muroya, Toshiki Kataoka, Ichiro Hasuo and Naohiko Hoshino
  • 学会等名: 5th Workshop on Syntax and Semantics of Low-Level Languages
  • 発表場所: Vienna, Austria
  • 年月日: 2014-07-13
• [学会発表] Generic Weakest Precondition Semantics from Monads Enriched with Order (2014)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 12th International Workshop on Coalgebraic Methods in Computer Science
  • 発表場所: Grenoble, France
  • 年月日: 2014-04-05 – 2014-04-06
  • 招待講演
• [学会発表] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13
  • 発表場所: Hotel Parco dei Principi, Rome, Italy
  • 年月日: 2013-01-25
• [学会発表] Semantics of Higher-Order Quantum Computation via Geometry of Interaction (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: Games for Logic and Programming Languages VIII, International Workshop （招待講演）
  • 発表場所: Queen Mary University of London, UK
  • 招待講演
• [学会発表] Coinductive Predicates and Final Sequences in a Fibration (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: Mathematical Foundations of Programming Semantics Twenty-ninth Conference
  • 発表場所: "Tulane University New Orleans, Louisiana, USA"
• [学会発表] 超準解析による物理情報システムの形式検証 ―離散から連続・ハイブリッドへ (2013)
  • 著者名/発表者名: 蓮尾 一郎
  • 学会等名: 日本数学会 秋季総合分科会 企画特別講演（招待講演）
  • 発表場所: 愛媛大学
  • 招待講演
• [学会発表] Exurcises in Nonstandard Static Analysis or Hybrid Systems (2012)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: Computer Aided Verification - 24th International Conference
  • 発表場所: LIC Berkeley, CA, USA
  • 年月日: 2012-07-12
• [学会発表] Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications (2012)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: ICE 2012 - 5th Interaction and Concurrency Experience
  • 発表場所: KTH Stockholm, Sweden(招待講演)
  • 年月日: 2012-06-16
• [図書] 圏論の歩き方 (2015)
  • 著者名/発表者名: 圏論の歩き方委員会 (編集)
  • 総ページ数: 295
  • 出版者: 日本評論社
• [図書] 越境する数学(第6章を執筆) (2013)
  • 著者名/発表者名: 西浦廉政編
  • 総ページ数: 230
  • 出版者: 岩波書店
• [備考] 東京大学蓮尾研ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/
• [備考] 研究代表者個人ウェブページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
• [備考] Personal Webpage of Ichiro Hasuo
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/index.html
• [備考] Hasuo Lab. Website
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/index.html?plain=false&lang=en&pos=title
• [備考] 蓮尾 一郎 研究者ページ
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
• [産業財産権] 制御入力値生成装置、制御入力値生成方法、および、プログラム (2014)
  • 発明者名: 赤崎拓未，蓮尾一郎，末永幸平
  • 権利者名: 科学技術振興機構
  • 産業財産権種類: 特許
  • 産業財産権番号: 2014-072623
  • 出願年月日: 2014-03-31