A unified theory and application of information hiding by program verification

• Project/Area Number: 18680003
• Research Category: Grant-in-Aid for Young Scientists (A)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: Tohoku University
• Principal Investigator: SUMII Eijiro Tohoku University, 大学院情報科学研究科, 准教授 (00333550)
• Project Period (FY): 2006 – 2008
• Project Status: Completed (Fiscal Year 2008)
• Budget Amount: ¥15,860,000 (Direct Cost: ¥12,200,000、Indirect Cost: ¥3,660,000); Fiscal Year 2008: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2007: ¥5,070,000 (Direct Cost: ¥3,900,000、Indirect Cost: ¥1,170,000); Fiscal Year 2006: ¥6,240,000 (Direct Cost: ¥4,800,000、Indirect Cost: ¥1,440,000)
• Keywords: プログラム言語 / 情報セキュリティ / プログラム等価性 / 双模倣 / ラムダ計算 / パイ計算 / 高階計算 / 型理論 / プログラミング言語 / 計算モデル / λ計算 / π計算 / 操作的意味論 / 文脈等価性 / 論理関係 / 環境双模倣 / 多相λ計算 / 高階π計算 / 存在型・再帰型システム / ポインタ演算 / C言語 / Fail-Safe C to Java / Objective Caml

Research Abstract

コンピュータプログラムやネットワークにおける暗号化や抽象化など、さまざまな形の情報保護の統一的基礎理論を研究した。特に、ループないし再帰関数、再帰型(リストや木など)、多相型ないしジェネリックス、抽象データ型ないしオブジェクトなど、幅広い現実的機能を有する計算体系における情報保護の数理論理学的証明手法を世界で初めて確立し、Journal of the ACMやIEEE LICSなど最高水準の国際論文誌・国際学会に採録・発表された。

Research Products

• [Journal Article] A Theory of Non-Monotone Memory (Or: Contexts for free) (2009)
  • Author(s): Eijiro Sumii
  • Journal Title: Proceedings of 18th European Symposium on Programming, (Lecture Notes in Computer Science, Springer-Verlag, Germany) vol. 550 Pages: 237-251
  • Peer Reviewed
• [Journal Article] A Theory of Non-Monotone Memory(Or : Contexts for free) (2009)
  • Author(s): Eijiro Sumii
  • Journal Title: Lecture Notes in Computer Science (Proceedings of 18th European Symposium on Programming) 5502 Pages: 237-251
  • Peer Reviewed
• [Journal Article] MinCamlコンパイラ (2008)
  • Author(s): 住井 英二郎
  • Journal Title: コンピュータソフトウェア, (岩波書店) 25巻2号 Pages: 28-38
  • NAID: 130004549107
  • Peer Reviewed
• [Journal Article] MinCamlコンパイラ (2008)
  • Author(s): 住井英二郎
  • Journal Title: コンピュータソフトウェア 25 Pages: 28-38
  • NAID: 130004549107
  • Peer Reviewed
• [Journal Article] Java言語への変換によるポインタ演算の安全な実装方式 (2008)
  • Author(s): 上嶋 祐紀, 住井 英二郎
  • Journal Title: コンピュータソフトウェア (採録決定)
  • NAID: 130004549129
  • Peer Reviewed
• [Journal Article] spi計算における暗号プロトコルの形式的検証 (2007)
  • Author(s): 住井 英二郎
  • Journal Title: 応用数理, (岩波書店) 17巻4号 Pages: 16-26
  • Peer Reviewed
• [Journal Article] A Bisimulation for Type Abstraction and Recursion (2007)
  • Author(s): Eijiro Sumii and Benjamin C. Pierce
  • Journal Title: Journal of the ACM, (issue 5, article 26) vol. 54 Pages: 1-43
  • Peer Reviewed
• [Journal Article] Environmental Bisimulations for Higher-Order Languages (2007)
  • Author(s): Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii
  • Journal Title: Proceedings of Twenty-Second Annual IEEE Symposium on Logic in Computer Science Pages: 293-302
  • Peer Reviewed
• [Journal Article] A Bisimulation for Dynamic Sealing. Theoretical Computer Science (2007)
  • Author(s): Eijiro Sumii and Benjamin C. Pierce
  • Journal Title: Elsevier Science, (issues 1-3) vol. 375 Pages: 169-192
  • Peer Reviewed
• [Journal Article] Logical Bisimulations and Functional Languages (2007)
  • Author(s): Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii
  • Journal Title: Post-Proceedings of IPM International Symposium on Fundamentals of Software Engineering, (Lecture Notes in Computer Science, Springer-Verlag, Germany) vol. 4767 Pages: 364-379
• [Journal Article] A Bisimulation for Type Abstraction and Recursion (2007)
  • Author(s): Eijiro Sumii and Benjamin C. Pierce
  • Journal Title: Journal of the ACM 54-5-26 Pages: 1-43
  • Peer Reviewed
• [Journal Article] A Bisimulation for Dynamic Sealing (2007)
  • Author(s): Eijiro Sumii, Benjamin C. Pierce
  • Journal Title: Theoretical Computer Science 375・1-3 Pages: 169-192
• [Journal Article] 型安全な通信ライブラリQuicksilverとその改良 (2007)
  • Author(s): 須藤尚稔, 住井英二郎
  • Journal Title: 第9回プログラミングおよびプログラミング言語ワークショップ論文集 Pages: 39-51
• [Journal Article] Javaへの変換による安全なC言語の実装 (2007)
  • Author(s): 上嶋祐紀, 住井英二郎
  • Journal Title: 第9回プログラミングおよびプログラミング言語ワークショップ論文集 Pages: 52-66
• [Presentation] A Theory of Non-Monotone Memory (Or : Contexts for free) (2009)
  • Author(s): Eijiro Sumii
  • Organizer: 18th European Symposium on Programming
  • Place of Presentation: ヨーク(イギリス)
  • Year and Date: 2009-03-26
• [Presentation] 型安全な通信ライブラリQuicksilverとその改良 (2007)
  • Author(s): 藤 尚稔, 住井 英二郎
  • Organizer: 日本ソフトウェア科学会 プログラミング論研究会 第9回プログラミングおよびプログラミング言語ワークショップ
  • Place of Presentation: 石川県加賀市
  • Year and Date: 2007-03-08
• [Presentation] spi計算における暗号プロトコルの形式的検証について (2006)
  • Author(s): 住井 英二郎
  • Organizer: 日本応用数理学会 数理的技法による情報セキュリティ研究部会 第二回研究集会
  • Place of Presentation: 東京大学駒場キャンパス
  • Year and Date: 2006-12-22
• [Presentation] 2時間で真似(まね)ぶ関数型言語のコンパイラ (2006)
  • Author(s): 住井 英二郎
  • Organizer: 日本ソフトウェア科学会 プログラミング論研究会 第44回プログラミングおよびプログラミング言語サマースクール
  • Place of Presentation: 東京大学本郷キャンパス
  • Year and Date: 2006-09-12
• [Remarks]
  • URL: http://www.kb.ecei.tohoku.ac.jp/~sumii/
• [Remarks]
  • URL: http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/