ストーン双対性と小宇宙原理による,モジュラーなシステム検証の一般理論

• 研究課題/領域番号: 23654033
• 研究種目: 挑戦的萌芽研究
• 配分区分: 基金
• 研究分野: 数学一般(含確率論・統計数学)
• 研究機関: 東京大学
• 研究代表者: 蓮尾 一郎 東京大学, 大学院・情報理工学系研究科, 講師 (60456762)
• 研究期間 (年度): 2011 – 2012
• 研究課題ステータス: 完了 (2012年度)
• 配分額: 3,770千円 (直接経費: 2,900千円、間接経費: 870千円); 2012年度: 1,430千円 (直接経費: 1,100千円、間接経費: 330千円); 2011年度: 2,340千円 (直接経費: 1,800千円、間接経費: 540千円)
• キーワード: システム検証 / ソフトウェア学 / 数学基礎論 / 数理論理学 / 応用数学 / 余代数 / 圏論的論理 / 不動点論理 / 圏論 / 仕様記述 / 国際研究者交流 オランダ / 国際研究者交流 イギリス / 国際研究者交流 ポーランド / 国際研究者交流 オーストリア

研究概要

小宇宙原理(システムのモジュラーな構成の数学的モデル)とストーン双対性(様相論理の数学的モデル)の組み合わせとその応用を当初目標として挙げたが,より広汎な視野で圏論・数学のシステム検証への貢献を志向した結果,ファイブレーション(圏論的論理で用いられる論理のモデル)における不動点論理の定式化とモデル検査への応用について新しい知見が得られたので,この新しい方向性の研究に注力し,最大不動点述語の圏論的構成に関する成果を得た.この成果を最小不動点を含む形に拡張すべく,研究を続行中である.

研究成果

• [雑誌論文] Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive Predicates and Final Sequences in a Fibration. To appear in Proc (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 雑誌名: MFPS XXIX. Electr. Notes in Theoretical Computer Science
  • 査読あり
• [雑誌論文] 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
  • 査読あり
• [雑誌論文] Coinductive Predicates and Final Sequences in a Fibration (2013)
  • 著者名/発表者名: Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs
  • 雑誌名: Proc. Mathematical Foundations of Programming Semantics, Twenty-ninth Conference, MFPS 2013, Electronic Notes in Theoretical Computer Science 巻: 未定
  • 査読あり
• [雑誌論文] 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
  • 査読あり
• [雑誌論文] Traces for Coalgebraic Components. (2011)
  • 著者名/発表者名: Ichiro Hasuo and Bart Jacobs
  • 雑誌名: Mathematical Structures in Computer Science 巻: 21 号: 2 ページ: 267-320
  • DOI: 10.1017/s0960129510000551
  • 査読あり
• [雑誌論文] The Microcosm Principle and Compositionality of GSOS-Based Component Calculi. Proc (2011)
  • 著者名/発表者名: Ichiro Hasuo
  • 雑誌名: Lecture Notes in Computer Science 巻: vol.6859 ページ: 222-236
  • DOI: 10.1007/978-3-642-22944-2_16
  • ISBN: 9783642229435, 9783642229442
  • 査読あり
• [雑誌論文] Programming with Infinitesimals : A While-Language for Hybrid System Modelin (2011)
  • 著者名/発表者名: Kohei Suenaga, Ichiro Hasuo
  • 雑誌名: Automata, Languages and Programming-38th International Colloquium, ICALP 2011 巻: 6756 ページ: 392-403
  • DOI: 10.1007/978-3-642-22012-8_31
  • ISBN: 9783642220111, 9783642220128
  • 査読あり
• [雑誌論文] Semantics of Higher-Order Quantum Computation via Geometry of Interaction. Proc (2011)
  • 著者名/発表者名: Ichiro Hasuo and Naohiko Hoshino.
  • 雑誌名: IEEE Computer Society 巻: 26 ページ: 237-246
  • DOI: 10.1109/lics.2011.26
  • 査読あり
• [学会発表] Categoical Geometry of Interaction and Quantum Programming (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際ワークショップGALOP2013
  • 発表場所: Imperial College London
  • 年月日: 2013-07-18
• [学会発表] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際会議POPL2013
  • 発表場所: Hotel Parco dei Principi, Rome, Italy.
  • 年月日: 2013-01-25
• [学会発表] Coinductive Predicates and Final Sequences in a Fibration (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際会議 MFPS XXIX
  • 発表場所: Tulane University, USA
• [学会発表] Coinductive Predicates and Final Sequences in a Fibration (2013)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: Mathematical Foundations of Programming Semantics, Twenty-ninth Conference, MFPS 2013
  • 発表場所: Tulane University, New Orleans, USA
• [学会発表] Exercises in Nonstandard Static Analysis of Hybrid Systems (2012)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際会議 CAV2012
  • 発表場所: UC Berkeley, USA(4) Ichiro Hasuo and Bart Jacobs. Traces
  • 年月日: 2012-07-12
• [学会発表] Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications (2012)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際ワークショップICE2012
  • 発表場所: KTH Stockholm, Sweden(招待講演)
  • 年月日: 2012-06-16
• [学会発表] The Microcosm Principle and Compositionality of GSOS-Based Component Calculi (2011)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: 国際会議 CALCO2011
  • 発表場所: University of Winchester, UK
  • 年月日: 2011-09-11
• [学会発表] Programming with Infinitesimals: A While-Language for Hybrid System Modeling (2011)
  • 著者名/発表者名: Kohei Suenaga
  • 学会等名: 国際会議ICALP2011
  • 発表場所: ETH Zurich, Switzerland (共著論文を共著者が発表)
  • 年月日: 2011-07-07
• [学会発表] Semantics of Higher-Order Quantum Computation via Geometry of Interaction (2011)
  • 著者名/発表者名: Naohiko Hoshino
  • 学会等名: 国際会議LICS2011
  • 発表場所: University of Toronto, Canada (共著論文を共著者が発表)
  • 年月日: 2011-06-23
• [学会発表] The Microcosm Principle and Compositionality of GSOS-Based Component Calculi (2011)
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: CALCO 2011
  • 発表場所: University of Winchester, UK
• [学会発表] Nonstandard Static Analysis: Discrete Verification Methodologies Transferred to Hybrid Applications
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: ICE 2012 – 5th Interaction and Concurrency Experience
  • 発表場所: KTH Stockholm, Sweden
  • 招待講演
• [学会発表] Exercises in Nonstandard Static Analysis of Hybrid Systems
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: Computer Aided Verification - 24th International Conference
  • 発表場所: UC Berkeley, CA, USA
• [学会発表] Hyperstream Processing Systems: Nonstandard Modeling of Continuous-Time Signals
  • 著者名/発表者名: Ichiro Hasuo
  • 学会等名: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13
  • 発表場所: Hotel Parco dei Principi, Rome, Italy
• [図書] 越境する数学 (2013)
  • 著者名/発表者名: 西浦廉政
  • 総ページ数: 230
  • 出版者: 岩波書店
• [図書] 越境する数学 （第6章を執筆） (2013)
  • 著者名/発表者名: 西浦廉政 編
  • 総ページ数: 230
  • 出版者: 岩波書店
• [備考]
  • URL: http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/