高階オープンシステムの数理的検証

• 研究課題/領域番号: 22300005
• 研究種目: 基盤研究(B)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: ソフトウエア
• 研究機関: 東北大学
• 研究代表者: 住井 英二郎 東北大学, 情報科学研究科, 教授 (00333550)
• 研究分担者: 寺内 多智弘 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (70447150)
• 研究期間 (年度): 2010-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 14,690千円 (直接経費: 11,300千円、間接経費: 3,390千円); 2014年度: 2,600千円 (直接経費: 2,000千円、間接経費: 600千円); 2013年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円); 2012年度: 3,120千円 (直接経費: 2,400千円、間接経費: 720千円); 2011年度: 2,860千円 (直接経費: 2,200千円、間接経費: 660千円); 2010年度: 3,250千円 (直接経費: 2,500千円、間接経費: 750千円)
• キーワード: 環境双模倣 / 並行・分散プロセス計算モデル / プログラム理論 / 形式手法 / 理論計算機科学 / 計算モデル / 分散プロセス計算 / 高階プログラム等価性証明 / 並行・分散プロセス計算 / プログラム意味論 / プロセス計算 / 並行分散システム / 形式的手法

研究成果の概要

複数のプロセスが並行に動作して、プロセス自身を通信することができ（高階）、かつ位置（ロケーション）の概念のある計算モデル（高階分散プロセス計算）において、「二つのシステムを外部から観察したときの動作が等しい」という振る舞い等価性を数理的に証明する、世界初の健全かつ完全な理論（環境双模倣）を確立、理論計算機科学のトップコンファレンスの一つACM/IEEE LICS 2012等に厳しい査読を経て論文が採択され、発表を行なった。

研究成果

• [雑誌論文] A Simple and Practical Linear Algebra Library with Static Size Checking (2014)
  • 著者名/発表者名: Akinori Abe, Eijiro Sumii
  • 雑誌名: Proceedings of The OCaml Users and Developers Workshop 巻: - ページ: 1-3
  • 査読あり / 謝辞記載あり
• [雑誌論文] A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions (2013)
  • 著者名/発表者名: Eijiro Sumii and Yuji Sato
  • 雑誌名: FCS'13: Workshop on Foundations of Computer Security (Informal Proceedings) 巻: - ページ: 68-82
  • 査読あり
• [雑誌論文] A Higher-Order Distributed Calculus with Name Creation (2012)
  • 著者名/発表者名: Adrien Pierard, Eijiro Sumii
  • 雑誌名: Proceedings of Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science 巻: 27 ページ: 531-540
  • DOI: 10.1109/lics.2012.63
  • 査読あり
• [雑誌論文] From Applicative to Environmental Bisimulation (2011)
  • 著者名/発表者名: Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii
  • 雑誌名: Electronic Notes in Theoretical Computer Science 巻: 276 ページ: 215-235
  • DOI: 10.1016/j.entcs.2011.09.023
  • 査読あり
• [雑誌論文] Sound Bisimulations for Higher-Order Distributed Process Calculus (2011)
  • 著者名/発表者名: Adrien Pierard, Eijiro Sumii
  • 雑誌名: Lecture Notes in Computer Science 巻: 6604 ページ: 123-137
  • 査読あり
• [雑誌論文] Environmental bisimulations for higher-order language (2011)
  • 著者名/発表者名: Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii
  • 雑誌名: ACM Transactions on Programming Language Systems 巻: 33(1)
  • 査読あり
• [雑誌論文] A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation (2010)
  • 著者名/発表者名: Eijiro Sumii
  • 雑誌名: Theoretical Computer Science 巻: 411(51-52) ページ: 4358-4378
  • 査読あり
• [学会発表] A Simple and Practical Linear Algebra Library with Static Size Checking (2014)
  • 著者名/発表者名: Eijiro Sumii
  • 学会等名: ACM SIGPLAN ML Family Workshop
  • 発表場所: Gothenburg, Sweden
  • 年月日: 2014-09-04
• [学会発表] Sound Bisimulations for Higher-Order Distributed Process Calculus (2011)
  • 著者名/発表者名: Adrien Pierard, Eijiro Sumii
  • 学会等名: 14th International Conference on Foundations of Software Science and Computation Structures
  • 発表場所: ドイツ・ザールブリュッケン
  • 年月日: 2011-03-28
• [学会発表] A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions
  • 著者名/発表者名: Eijiro Sumii
  • 学会等名: FCS'13: Workshop on Foundations of Computer Security
  • 発表場所: Tulane University, New Orleans, USA
• [学会発表] Environmental Bisimulation and Its Open Problems
  • 著者名/発表者名: Eijiro Sumii
  • 学会等名: IFIP Working Group 2.8
  • 発表場所: Aussois, France
• [学会発表] A Higher-Order Distributed Calculus with Name Creation
  • 著者名/発表者名: Adrien Pierard, Eijiro Sumii
  • 学会等名: Twenty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science
  • 発表場所: Dubrovnik, Croatia
• [学会発表] From Applicative to Environmental Bisimulation
  • 著者名/発表者名: Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii
  • 学会等名: Mathematical Foundations of Programming Semantics
  • 発表場所: Carnegie Mellon University, Pittsburgh, PA, USA