研究者詳細

顔写真

スミイ　エイジロウ
住井　英二郎
Eijiro Sumii
所属
大学院情報科学研究科　情報基礎科学専攻　ソフトウェア科学講座（ソフトウェア基礎科学分野）
職名
教授
学位

  • 博士（情報理工学）（東京大学）

  • 修士（理学）（東京大学）

経歴 6

  • 2010年11月 ～ 継続中
    日本学術会議　特任連携会員（～2014年9月）・連携会員（2014年10月～） 若手アカデミー活動検討分科会委員(2010-2011), 若手アカデミー委員会委員(2011-2014), 若手アカデミー幹事(2015-2017), 若手アカデミー世話人(2017)他

  • 2005年5月 ～ 継続中
    東北大学大学院情報科学研究科　助教授（～2007年3月）・准教授（職名変更、2007年4月～2014年4月）・教授（2014年5月～）

  • 2003年4月 ～ 2005年3月
    Department of Computer and Information Science, School of Engineering and Applied Science, ペンシルバニア大学　Research Associate

  • 2001年4月 ～ 2003年3月
    東京大学大学院情報学環　助手

  • 2000年4月 ～ 2001年3月
    日本学術振興会　特別研究員(DC1)

  • 2000年4月 ～ 2001年3月
    Department of Computer and Information Science, School of Engineering and Applied Science, ペンシルバニア大学　Visiting Scholar

︎全件表示 ︎最初の5件までを表示

学歴 2

  • 東京大学　理学系研究科　情報科学専攻

    ～ 2001年3月

  • 東京大学　理学部　情報科学科

    ～ 1998年3月

委員歴 48

  • Journal of Functional Programming (Cambridge University Press)　Editor

    2018年7月 ～ 継続中

  • Journal of Functional Programming (Cambridge University Press)　Guest Editor

    2016年9月 ～ 継続中

  • International Federation for Information Processing (IFIP) Working Group (WG) 2.8 (Functional Programming)　Member

    2014年8月 ～ 継続中

  • 日本ソフトウェア科学会　学会誌『コンピュータソフトウェア』（岩波書店）編集委員

    2009年4月 ～ 継続中

  • 21st ACM SIGPLAN International Conference on Functional Programming　Steering Committee Member

    2014年12月 ～ 2018年10月

  • International Symposium on Functional and Logic Programming (FLOPS)　Steering Committee Chair

    2014年6月 ～ 2016年3月

  • 日本ソフトウェア科学会 プログラミング論研究会　運営委員長

    2014年4月 ～ 2016年3月

  • 日本ソフトウェア科学会 プログラミング論研究会　運営委員

    2011年4月 ～ 2016年3月

  • Journal of Functional Programming (Cambridge University Press)　Editorial Board Member

    2009年1月 ～ 2013年12月

  • The ACM SIGPLAN Workshop on ML　Steering Committee Chair

    2010年10月 ～ 2011年9月

  • The ACM SIGPLAN Workshop on ML　Steering Committee Member

    2008年9月 ～ 2011年9月

  • 情報処理学会　東北支部 会計幹事

    2009年4月 ～ 2011年3月

  • APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems　Program Committee Member

    2010年11月 ～ 2010年12月

  • ESOP'08: 17th European Symposium on Programming　Program Committee Member

    2008年3月 ～ 2008年4月

  • The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007)　Program Committee Member

    2007年11月 ～ 2007年12月

  • The Fifth ASIAN Symposium on Programming Languages and Systems (APLAS 2007)　Poster Chair

    2007年11月 ～ 2007年12月

  • 日本ソフトウェア科学会　企画委員

    2001年10月 ～ 2003年3月

  • The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)　Program Committee Member

    2017年1月 ～

  • 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)　Program Chair

    2016年9月 ～

  • 日本ソフトウェア科学会第32回大会　プログラム委員

    2015年9月 ～

  • 日本ソフトウェア科学会 第31回大会　プログラム委員

    2014年9月 ～

  • WPTE 2014: First International Workshop on Rewriting Techniques for Program Transformations and Evaluation　Program Committee Member

    2014年7月 ～

  • Twelfth International Symposium on Functional and Logic Programming (FLOPS 2014)　Program Co-Chair, General Chair

    2014年6月 ～

  • ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation (PEPM'14)　Program Committee Member

    2014年1月 ～

  • POPL 2013: 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages　External Review Committee: Member

    2013年1月 ～

  • HOPE 2012: The 1st ACM SIGPLAN Workshop on Higher-Order Programming with Effects　Program Committee Member

    2012年9月 ～

  • Scheme 2012: Workshop on Scheme and Functional Programming　Program Committee Member

    2012年9月 ～

  • ICFP 2012: The 17th ACM SIGPLAN International Conference on Functional Programming　Program Committee Member

    2012年9月 ～

  • Haskell Symposium 2012　Program Committee Member

    2012年9月 ～

  • Fourteenth International Symposium on Practical Aspects of Declarative Languages: PADL'12　Program Committee Member

    2012年1月 ～

  • ICFP 2011: The 16th ACM SIGPLAN International Conference on Functional Programming　Programming Contest Chair

    2011年9月 ～

  • 日本ソフトウェア科学会第27回大会　プログラム委員

    2010年9月 ～

  • FLOPS 2010: Tenth International Symposium on Functional and Logic Programming　Local Chair

    2010年4月 ～

  • The 2008 ACM SIGPLAN Workshop on ML　Program Chair

    2008年9月 ～

  • ACM SIGPLAN Third Workshop on Programming Languages and Analysis for Security (PLAS 2008)　Program Committee Member

    2008年6月 ～

  • 第10回プログラミングおよびプログラミング言語ワークショップ: PPL2008　プログラム共同委員長

    2008年3月 ～

  • The 35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages　Program Committee Member

    2008年1月 ～

  • Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis: FCS-ARSPA'07　Program Committee Member

    2007年7月 ～

  • ACM SIGPLAN Workshop on Programming Languages and Analysis for Security　Program Committee Member

    2007年6月 ～

  • The Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006)　Poster Chair

    2006年11月 ～

  • ESORICS 2006: 11th European Symposium On Research In Computer Security　Program Committee Member

    2006年9月 ～

  • Eighth International Symposium on Functional and Logic Programming: FLOPS 2006　Program Committee Member

    2006年4月 ～

  • 第８回プログラミングおよびプログラミング言語ワークショップ(PPL2006)　プログラム委員

    2006年3月 ～

  • 日本ソフトウェア科学会第22回大会　プログラム委員

    2005年9月 ～

  • The 2005 ACM SIGPLAN Workshop on ML　Program Committee Member

    2005年9月 ～

  • 第7回プログラミングおよびプログラミング言語ワークショップ(PPL2005)　プログラム委員

    2005年3月 ～

  • The 2004 International Conference on Functional Programming (ICFP)　Programming Contest Organizer

    2004年9月 ～

  • 8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003)　Program Committee Member

    2003年8月 ～

︎全件表示 ︎最初の5件までを表示

所属学協会 3

  • 情報処理学会

  • 日本ソフトウェア科学会

  • Association for Computing Machinery

研究キーワード 7

  • π計算

  • λ計算

  • 型システム

  • セキュリティ

  • 関数型プログラミング

  • ソフトウェア基礎科学

  • プログラミング言語理論

研究分野 2

  • 情報通信 / ソフトウェア /

  • 情報通信 / 情報学基礎論 /

受賞 13

  1. ソフトウエアジャパンアワード

    2014年2月4日　情報処理学会

  2. 第9回（平成24年度）日本学術振興会賞

    2013年2月4日　日本学術振興会

  3. 第11回船井学術賞

    2012年4月14日　船井情報科学振興財団

  4. 第25回日本IBM科学賞（コンピューター・サイエンス分野）

    2011年12月1日　日本IBM

  5. 第1回RIEC Award東北大学研究者賞

    2011年11月18日　東北大学電気通信研究所

  6. 日本ソフトウェア科学会第15回論文賞

    2011年6月9日　日本ソフトウェア科学会

  7. 第2回マイクロソフトリサーチ日本情報学研究賞（基礎的情報学分野）

    2010年7月26日　マイクロソフト株式会社

  8. 第7回船井情報科学奨励賞

    2008年4月19日　船井情報科学振興財団

  9. 第1回野口研究奨励賞

    2006年5月10日　情報処理学会東北支部

  10. 2004年度上期未踏ソフトウェア創造事業天才プログラマー／スーパークリエータ

    2005年5月18日　情報処理推進機構

  11. The Fifth ICFP Programming Contest (1st Place)

    2002年10月5日　ACM SIGPLAN International Conference on Functional Programming

  12. 日本ソフトウェア科学会第3回プログラミングおよびプログラミング言語ワークショップ論文賞

    2001年2月23日　日本ソフトウェア科学会

  13. The Third Annual ICFP Programming Contest (1st Place)

    2000年9月19日　ACM SIGPLAN International Conference on Functional Programming

︎全件表示 ︎最初の5件までを表示

論文 67

  1. Polymorphic Gradual Typing with Holes

    KIM Jaebyeog, SUMII Eijiro

    日本ソフトウェア科学会大会講演論文集(Web)　37th　2020年

    ISSN：1349-3515

  2. 型システムを用いたロックフリースタックの検証

    佐藤駿太朗, 住井英二郎

    日本ソフトウェア科学会大会講演論文集(Web)　37th　2020年

    ISSN：1349-3515

  3. 3A04 新入生オリエンテーション合宿におけるPBL研修:東北大学工学部電気情報物理工学科における初年次教育

    中村 健二, 齊藤 伸, 住井 英二郎, 渡邉 高志, 陳 強, 伊藤 彰則

    工学教育研究講演会講演論文集　2019　276-277　2019年

    出版者・発行元： 公益社団法人 日本工学教育協会

    DOI： 10.20549/jseeja.2019.0_276 　

    ISSN：2189-8928

  4. Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. 査読有り

    Masayuki Mizuno, Eijiro Sumii

    Programming Languages and Systems - 17th Asian Symposium, APLAS 2019, Nusa Dua, Bali, Indonesia, December 1-4, 2019, Proceedings　181-201　2019年

    出版者・発行元： Springer

    DOI： 10.1007/978-3-030-34175-6_10 　

  5. Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name 査読有り

    Masayuki Mizuno, Eijiro Sumii

    Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings　1-16　2018年

    出版者・発行元： Springer

    DOI： 10.1007/978-3-319-90686-7_1 　

  6. 無限の入出力を行う関数型プログラムの K正規化の形式的検証

    水野雅之, 住井英二郎

    コンピュータソフトウェア　34　(2)　2_114‐2_119(J‐STAGE)　2017年

    DOI： 10.11309/jssst.34.2_114 　

    ISSN：0289-6540

  7. A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc 査読有り

    Taichi Yachi, Eijiro Sumii

    Programming Languages and Systems - 14th Asian Symposium, APLAS 2016, Hanoi, Vietnam, November 21-23, 2016, Proceedings, Lecture Notes in Computer Science　10017　171-186　2016年

    DOI： 10.1007/978-3-319-47958-3_10 　

  8. 無限の入出力を行う関数型プログラムのK正規化の形式的検証

    水野, 雅之, 住井, 英二郎

    日本ソフトウェア科学会大会論文集　33　475-480　2016年

  9. Specialization of Generic Array Accesses After Inlining.

    Ryohei Tokuda, Eijiro Sumii, Akinori Abe

    45-53　2015年

    DOI： 10.4204/EPTCS.241.4 　

  10. A Simple and Practical Linear Algebra Library Interface with Static Size Checking 査読有り

    Akinori Abe, Eijiro Sumii

    Proceedings ML Family/OCaml Users and Developers workshops, ML/OCaml 2015, Gothenburg, Sweden, September 4-5, 2014., EPTCS　198　1-21　2015年

    DOI： 10.4204/EPTCS.198.1 　

  11. Call/ccを含む型無しラムダ計算における文脈等価性の一証明手法

    谷内, 太一, 住井, 英二郎

    日本ソフトウェア科学会大会論文集　32　1-7　2015年

  12. A Simple and Practical Linear Algebra Library Interface with Static Size Checking 査読有り

    Akinori Abe, Eijiro Sumii

    The OCaml Users and Developers Workshop　1-3　2014年

  13. 単純かつ実用的な静的サイズ検査つき線形代数演算ライブラリ 査読有り

    阿部 晃典, 住井 英二郎

    第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集　1-16　2014年

  14. A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions 査読有り

    Eijiro Sumii, Yuji Sato

    FCS 2013 Workshop on Foundations of Computer Security (Informal Proceedings)　68-82　2013年

  15. 対応表明つきプロトコル記述からSpiCAへの複数セッションを考慮した変換 査読有り

    佐藤 悠史, 住井 英二郎

    第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)論文集　1-15　2013年

  16. A Higher-Order Distributed Calculus with Name Creation 査読有り

    Adrien Piérard, Eijiro Sumii

    Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012　531-540　2012年

    DOI： 10.1109/LICS.2012.63 　

  17. From Applicative to Environmental Bisimulation 査読有り

    Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii

    HLCL '98, 3rd International Workshop on High-Level Concurrent Languages (Satellite Workshop of CONCUR '98), Electr. Notes Theor. Comput. Sci.　276　215-235　2011年

    DOI： 10.1016/j.entcs.2011.09.023 　

  18. Sound Bisimulations for Higher-Order Distributed Process Calculus 査読有り

    Adrien Piérard, Eijiro Sumii

    Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Procee　6604　123-137　2011年

    DOI： 10.1007/978-3-642-19805-2_9 　

  19. Environmental bisimulations for higher-order languages 査読有り

    Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

    ACM Trans. Program. Lang. Syst.　33　(1)　5:1-5:69　2011年

    DOI： 10.1145/1889997.1890002 　

    詳細を見る 詳細を閉じる

    Contains a number of typographical errors introduced by the copy editor (which the authors did not have time to correct)

  20. Sound Bisimulations for Higher-Order Distributed Process Calculus

    Adrien Piérard, Eijiro Sumii

    CoRR　abs/1006.4943　1-15　2010年

  21. Limitations of Applicative Bisimulation (Preliminary Report) 招待有り

    Vasileios Koutavas, Paul Blain Levy, Eijiro Sumii

    Modelling, Controlling and Reasoning About State, 29.08. - 03.09.2010, Dagstuhl Seminar Proceedings　10351　1-9　2010年

  22. A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation 査読有り

    Eijiro Sumii

    Theor. Comput. Sci.　411　(51-52)　4358-4378　2010年

    DOI： 10.1016/j.tcs.2010.09.009 　

  23. The Higher-Order, Call-by-Value Applied Pi-Calculus 査読有り

    Nobuyuki Sato, Eijiro Sumii

    Programming Languages and Systems, 7th Asian Symposium, APLAS 2009, Seoul, Korea, December 14-16, 2009. Proceedings, Lecture Notes in Computer Science　5904　311-326　2009年

    DOI： 10.1007/978-3-642-10672-9_22 　

  24. A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References 査読有り

    Eijiro Sumii

    Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7-11, 2009. Proceedings, Lecture Notes in Computer Science　5771　455-469　2009年

    DOI： 10.1007/978-3-642-04027-6_33 　

  25. A Theory of Non-monotone Memory (Or: Contexts for free) 査読有り

    Eijiro Sumii

    Programming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, Lecture Notes in Computer Scienc　5502　237-251　2009年

    DOI： 10.1007/978-3-642-00590-9_18 　

  26. Java言語への変換によるポインタ演算の安全な実装方式 査読有り

    上嶋, 祐紀, 住井, 英二郎

    コンピュータ ソフトウェア　26　(1)　139-154　2009年

    DOI： 10.11309/jssst.26.1_139 　

  27. ＭｉｎＣａｍｌコンパイラ 査読有り

    住井, 英二郎

    コンピュータ ソフトウェア　25　(2)　28-38　2008年

    DOI： 10.11309/jssst.25.2_28 　

  28. A bisimulation for dynamic sealing 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    Theor. Comput. Sci.　375　(1-3)　169-192　2007年

    DOI： 10.1016/j.tcs.2006.12.032 　

  29. Logical Bisimulations and Functional Languages 招待有り

    Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

    International Symposium on Fundamentals of Software Engineering, International Symposium, FSEN 2007, Tehran, Iran, April 17-19, 2007, Proceedings, Lecture Notes in Computer Science　4767　364-379　2007年

    DOI： 10.1007/978-3-540-75698-9_24 　

  30. Environmental Bisimulations for Higher-Order Languages 査読有り

    Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

    22nd IEEE Symposium on Logic in Computer Science (LICS 2007), 10-12 July 2007, Wroclaw, Poland, Proceedings　293-302　2007年

    DOI： 10.1109/LICS.2007.17 　

  31. Javaへの変換による安全なC言語の実装 査読有り

    上嶋祐紀, 住井英二郎

    第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)論文集　52-66　2007年

  32. 型安全な通信ライブラリQuicksilverとその改良 査読有り

    須藤尚稔, 住井英二郎

    第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)論文集　39-51　2007年

  33. Quicksilver/OCaml: A Poor Man's Type-Safe and Abstraction-Secure Communication Library (Work in Progress)

    Hisatoshi Sutou, Eijiro Sumii

    Manuscript　2007年

  34. A bisimulation for type abstraction and recursion 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    J. ACM　54　(5)　26:1-26:43　2007年

    DOI： 10.1145/1284320.1284325 　

  35. MinCaml: a simple and efficient compiler for a minimal functional language 査読有り

    Eijiro Sumii

    Proceedings of the 2005 workshop on Functional and declarative programming in education, Tallinn, Estonia, September 25 - 25, 2005　27-38　2005年

    DOI： 10.1145/1085114.1085122 　

  36. A bisimulation for type abstraction and recursion 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005　63-74　2005年

    DOI： 10.1145/1040305.1040311 　

  37. A bisimulation for dynamic sealing 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004　161-172　2004年

    DOI： 10.1145/964001.964015 　

  38. セキュリティプロトコルの略式記法からspi 計算への変換 査読有り

    住井英二郎, 立沢, 秀晃, 米澤, 明憲

    情報処理学会論文誌プログラミング（PRO）　45　(12)　1-10　2004年

  39. 例外処理機構を備えた命令型言語のCPS変換とその定式化 査読有り

    住井英二郎, 大根田裕一, 米澤, 明憲

    情報処理学会論文誌プログラミング（PRO）　45　(12)　67-82　2004年

  40. The Extension of ML with Hypothetical Views for Discovery Science: Formalization and Implementation 査読有り

    Eijiro Sumii, Hideo Bannai

    Journal of Functional and Logic Programming　2003　1-22　2003年

  41. The Interface Definition Language for Fail-Safe C 査読有り

    Kohei Suenaga, Yutaka Oiwa, Eijiro Sumii, Akinori Yonezawa

    Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium, ISSS 2003, Tokyo, Japan, November 4-6, 2003, Revised Papers, Lecture Notes in Computer Science　3233　192-208　2003年

    DOI： 10.1007/978-3-540-37621-7_10 　

  42. テキスト処理言語における文字列のための正規表現型 査読有り

    田渕, 直, 住井英二郎, 米澤, 明憲

    情報処理学会論文誌プログラミング（PRO）　44　(2)　1-12　2003年

  43. C++テンプレートを分割コンパイルするためのアプローチ

    増山, 隆, 住井英二郎, 米澤, 明憲

    情報処理学会論文誌プログラミング（PRO）　44　(2)　42-42　2003年

  44. Fail-Safe Cのためのインターフェイス定義言語 査読有り

    末永幸平, 大岩寛, 住井英二郎, 米澤明憲

    第5回プログラミングおよびプログラミング言語ワークショップ(PPL 2003)論文集　135-148　2003年

  45. Logical Relations for Encryption 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    Journal of Computer Security　11　(4)　521-554　2003年

  46. Regular Expression Types for Strings in a Text Processing Language 査読有り

    Naoshi Tabuchi, Eijiro Sumii, Akinori Yonezawa

    TIP'02, International Workshop in Types in Programming, Electr. Notes Theor. Comput. Sci.　75　95-113　2002年

    DOI： 10.1016/S1571-0661(04)80781-3 　

    詳細を見る 詳細を閉じる

    Errata: http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/xperl.err.txt

  47. VMλ: A Functional Calculusfor Scientific Discovery 査読有り

    Eijiro Sumii, Hideo Bannai

    Functional and Logic Programming, 6th International Symposium, FLOPS 2002, Aizu, Japan, September 15-17, 2002, Proceedings, Lecture Notes in Computer Science　2441　290-304　2002年

    DOI： 10.1007/3-540-45788-7_18 　

  48. Fail-Safe ANSI-C Compiler: An Approach to Making C Programs Secure: Progress Report 査読有り

    Yutaka Oiwa, Tatsurou Sekiguchi, Eijiro Sumii, Akinori Yonezawa

    Software Security -- Theories and Systems, Mext-NSF-JSPS International Symposium, ISSS 2002, Tokyo, Japan, November 8-10, 2002, Revised Papers, Lecture Notes in Computer Science　2609　133-153　2002年

    DOI： 10.1007/3-540-36532-X_9 　

  49. Supporting objects in run-time bytecode specialization 査読有り

    Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa

    Proceedings of the ACM SIGPLAN ASIA-PEPM 2002, Asian Symposium on Partial Evaluation and Semantics-Based Program Manipulation, Aizu, Japan, September 12-14, 2002　50-60　2002年

    DOI： 10.1145/568173.568179 　

  50. 安全性を保証する ANSI-C 実行系の実装手法 査読有り

    大岩 寛, 住井 英二郎, 米澤 明憲

    コンピュータ ソフトウェア　19　(3)　195-200　2002年

    DOI： 10.11309/jssst.19.195 　

  51. Linux/TAL: 型付きアセンブリプログラムのカーネルモード実行方式 査読有り

    前田 俊行, 住井 英二郎, 米澤 明憲

    第4回プログラミングおよびプログラミング言語ワークショップ(PPL 2002)論文集　62-73　2002年

  52. A Scheme-to-Java Translator with Soft Typing

    Akihito Nagata, Eijiro Sumii, Akinori Yonezawa

    Manuscript　1-7　2002年

  53. C++テンプレートを分割コンパイルするためのアプローチ

    増山 隆, 住井 英二郎, 米澤 明憲

    Manuscript　1-16　2002年

  54. Javaバイトコードにおけるオブジェクト使用解析のための型システム

    浜中 信行, 住井 英二郎, 小林 直樹, 米澤 明憲

    第4回プログラミングおよびプログラミング言語ワークショップ(PPL 2002)論文集　74-88　2002年

  55. A Hybrid Approach to Online and Offline Partial Evaluation 査読有り

    Eijiro Sumii, Naoki Kobayashi

    Higher-Order and Symbolic Computation　14　(2-3)　101-142　2001年

    DOI： 10.1023/A:1012984529382 　

  56. VMλ: a Functional Calculus for Scientific Discovery

    Eijiro Sumii, Hideo Bannai

    The Second Asian Workshop on Programming Languages and Systems, APLAS'01, Korea Advanced Institute of Science and Technology, Daejeon, Korea, December 17-18, 2001, Proceedings　265-275　2001年

  57. A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation 査読有り

    Daisuke Hoshina, Eijiro Sumii, Akinori Yonezawa

    Theoretical Aspects of Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan, October 29-31, 2001, Proceedings, Lecture Notes in Computer Science　2215　64-81　2001年

    DOI： 10.1007/3-540-45500-0_3 　

  58. Logical Relations for Encryption 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    Computer Security Foundations Workshop, 2001. Proceedings. 14th IEEE　256-269　2001年

    DOI： 10.1109/CSFW.2001.930151 　

  59. The Cryptographic lambda-Calculus: Syntax, Semantics, Type System and Logical Relations 査読有り

    Eijiro Sumii, Benjamin C. Pierce

    第3回プログラミングおよびプログラミング言語ワークショップ(PPL 2001)論文集　97-108　2001年

  60. 安全性を保証するANSI-C実行系の実装手法

    大岩 寛, 住井 英二郎, 米澤 明憲

    日本ソフトウェア科学会大会論文集　18　1-5　2001年

  61. Supporting Objects in Run-time Bytecode Specialization

    Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa

    日本ソフトウェア科学会大会論文集　18　1-4　2001年

  62. An Implicitly-Typed Deadlock-Free Process Calculus 査読有り

    Naoki Kobayashi, Shin Saito, Eijiro Sumii

    CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, Lecture Notes in Computer Science　1877　489-503　2000年

    DOI： 10.1007/3-540-44618-4_35 　

  63. Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract) 査読有り

    Eijiro Sumii, Naoki Kobayashi

    Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '00), Boston, Massachusetts, USA, January 22-23, 2000　12-21　2000年

    DOI： 10.1145/328690.328694 　

  64. 動的に型付けされた言語のためのオンラインな型主導部分評価(特集●プログラミング及びプログラミング言語) 査読有り

    住井 英二郎, 小林 直樹

    コンピュータソフトウェア　17　(3)　230-254　2000年

    DOI： 10.11309/jssst.17.230 　

  65. An Implementation of Transparent Migration on Standard Scheme 査読有り

    Eijiro Sumii

    Proceedings of the Workshop on Scheme and Functional Programming 2000　61-63　2000年

  66. 動的に型付けされた言語のためのオンラインな型主導部分評価 査読有り

    Eijiro Sumii, Naoki Kobayashi

    第1回プログラミングおよびプログラミング言語ワークショップ(PPL 1999)論文集　55-66　1999年

  67. A Generalized Deadlock-Free Process Calculus 査読有り

    Eijiro Sumii, Naoki Kobayashi

    Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVII), Electr. Notes Theor. Comput. Sci.　16　(3)　225-247　1998年

    DOI： 10.1016/S1571-0661(04)00144-6 　

︎全件表示 ︎最初の5件までを表示

MISC 15

  1. 第1回アジア若手アカデミー会合参加報告

    住井 英二郎

    学術の動向　22　(9)　9_105-9_106　2017年

    出版者・発行元： 公益財団法人 日本学術協力財団

    DOI： 10.5363/tits.22.9_105 　

    ISSN： 1342-3363

  2. パネルディスカッション「若手科学者と研究費」 (特集 若手科学者の現在と課題 : 若手科学者サミット)

    住井, 英二郎

    学術の動向 = Trends in the sciences　22　(12)　62-64　2017年

  3. 私の非研究

    住井, 英二郎

    コンピュータ ソフトウェア　33　(2)　2_92-2_93　2016年

    DOI： 10.11309/jssst.33.2_92 　

  4. 若手アカデミーの発足

    住井, 英二郎

    学術の動向　21　(3)　3_118-3_120　2016年

    DOI： 10.5363/tits.21.3_118 　

  5. Preface for special section from FLOPS 2014

    Michael Codish, Eijiro Sumii

    J. Funct. Program.　26　(e14)　1-2　2016年

    DOI： 10.1017/S0956796816000149 　

  6. いまさら聞けない! コンピュータの数学：1. プログラミング言語の数学

    住井, 英二郎

    情報処理　56　(5)　434-437　2015年

  7. OCaml入門：“O”が示すもの

    住井 英二郎

    日経ソフトウエア　39-44　2014年11月

    出版者・発行元： 日経BP社

  8. 特集「プログラミングおよびプログラミング言語」の編集にあたって

    住井 英二郎, 首藤 一幸

    コンピュータソフトウェア　26　(2)　1-2　2009年

    DOI： 10.11309/jssst.26.2_1 　

  9. spi計算における暗号プロトコルの形式的検証(<特集>数理的技法による情報セキュリティ)

    住井, 英二郎

    応用数理　17　(4)　280-290　2007年

  10. 安全なC言語～プログラミング言語研究の前線から

    住井 英二郎

    オープンソースマガジン　67-73　2006年10月

    出版者・発行元： ソフトバンク クリエイティブ

  11. 数理科学的バグ撲滅方法論のすすめ

    住井 英二郎

    日経ITPro　2006年8月

    出版者・発行元： 日経BP社

    詳細を見る 詳細を閉じる

    第1回（2006年8月）～第16回（2007年11月）

  12. 暗号化通信のｓｐｉ計算による形式的検証

    住井, 英二郎

    コンピュータ ソフトウェア　20　(6)　607-616　2003年

    DOI： 10.11309/jssst.20.607 　

  13. TACS2001およびManfred Paul賞授賞式

    五十嵐淳, 住井英二郎

    情報処理　43　(2)　200-201　2002年

  14. CSFW-14報告

    住井, 英二郎

    コンピュータ ソフトウェア　18　(6)　637-641　2001年

    DOI： 10.11309/jssst.18.637 　

  15. POPL/PEPM'99会議報告

    住井 英二郎, 小林 直樹

    コンピュータソフトウェア　16　(4)　372-377　1999年

︎全件表示 ︎最初の5件までを表示

書籍等出版物 6

  1. プログラム意味論の基礎

    小林, 直樹, 住井, 英二郎

    サイエンス社　2020年8月

    ISBN: 9784781914831

  2. Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016

    Jacques Garrigue, Gabriele Keller, Eijiro Sumii

    ACM　2016年

    ISBN: 9781450342193

  3. Functional and Logic Programming - 12th International Symposium, FLOPS 2014, Kanazawa, Japan, June 4-6, 2014. Proceedings (Lecture Notes in Computer Science 8475)

    Michael Codish, Eijiro Sumii

    Springer　2014年

    DOI： 10.1007/978-3-319-07151-0 　

    ISBN: 9783319071503

  4. 型システム入門 : プログラミング言語と型の理論

    Benjamin C, Pierce 著, 住井英二郎, 遠藤侑介, 他

    オーム社　2013年

    ISBN: 9784274069116

  5. 数理的技法による情報セキュリティ

    萩谷昌巳, 塚田恭章, 住井英二郎

    共立出版　2010年

    ISBN: 9784320019508

  6. Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008

    Eijiro Sumii

    ACM　2008年

    ISBN: 9781605580623

︎全件表示 ︎最初の5件までを表示

講演・口頭発表等 85

  1. Hedged bisimulationの非対称鍵暗号による拡張

    続 隼人, 住井 英二郎

    第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）　2025年3月7日

  2. セキュリティ束の動的拡張が可能なπ計算の型ベース情報流解析

    織田 幸弘, 住井 英二郎

    第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）　2025年3月6日

  3. RustへのFractional Ownershipの動的検査の導入

    馬場 風汰, 住井 英二郎

    第26回プログラミングおよびプログラミング言語ワークショップ（PPL 2024）　2024年3月6日

  4. 構造化グラフの正規化の証明

    柳沢 大貴, 住井 英二郎

    第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023年3月

  5. 複数参加者非同期セッション型の一般プロセス型への変換

    細川 万里奈, 住井 英二郎

    第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023年3月

  6. LEGO Education SPIKE PrimeのMicroPython環境における関数型リアクティブプログラミング

    中里 匡亮, 住井 英二郎

    第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023年3月

  7. 定理証明支援器Coqを用いた計算量の証明の改良

    中村 悠紀, 住井 英二郎

    PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021年3月10日

  8. MetaOCamlによる自律型ロボットのためのCコード生成

    山本 うらん, 住井 英二郎

    PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021年3月10日

  9. SMTソルバーを利用した算術式を含む高階関数の等価性検証手法

    遠藤 瑛輔, 住井 英二郎

    PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021年3月9日

  10. Progress report: Ruby 3における静的型解析の実現に向けて

    遠藤 侑介, 松本 宗太郎, 上野 雄大, 住井 英二郎, 松本 行弘

    第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019年3月6日

  11. ブロックチェーン合意形成プロトコルのCoqによる証明からのコード抽出

    木村 朝輝, 住井 英二郎

    第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019年3月6日

  12. NetKAT with Cryptography

    菅原 慎之介, 住井 英二郎

    第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019年3月6日

  13. Experiences in the Young Academy of Japan 国際会議

    Eijiro Sumii

    2017 Y-KAST - YAJ Bilateral Workshop on "Institutional and Scientific Challenges for Young Scientists in Asia"　2017年3月15日

  14. Established NYAs in Asia: Success Story and Initiatives 国際会議

    Nana Saleh, Pooja Gupta, Udi Sommer, Eijiro Sumii, Jwa-Min Nam, Abhi Veerakumarasivam, Aftab Ahmad, Thomas Edison E, Dela Cruz, Numpon Mahayotsanun, Yusuf Baran, Tran Quang Huy

    1st Asian National Young Academy Meeting: Advancing Synergies in Asian NYAs　2016年12月15日

  15. Program Chair Report 国際会議

    Eijiro Sumii

    ICFP 2016: The 21st ACM SIGPLAN International Conference on Functional Programming　2016年9月18日

  16. 機械学習による関数型ブーリアンプログラムの型推論

    阿部 晃典, 住井 英二郎

    第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）　2016年3月7日

  17. プログラムの論理

    住井 英二郎

    第61回情報科学談話会　2015年12月3日

  18. Global Young Academy: The voice of young scientists around the world 国際会議

    Eijiro Sumii

    The Third UN World Conference on Disaster Risk Reduction, Science and Technology Major Group Booth　2015年3月17日

  19. An Experiment for Duplication of Polymorphic Functions in OCaml 国際会議

    Ryohei Tokuda, Eijiro Sumii

    APLAS 2014: 12th Asian Symposium on Programming Languages and Systems　2014年11月17日

  20. Normalizing Structured Graphs 国際会議

    Eijiro Sumii, Kazuma Kikuchi

    IFIP Working Group 2.8 32nd meeting　2014年8月11日

  21. いわゆる「情報系」研究者・技術者のキャリアパスについて

    住井 英二郎

    筑波大学附属駒場高等学校 進路懇談会　2014年7月5日

  22. Opening 国際会議

    Eijiro Sumii

    Twelfth International Symposium on Functional and Logic Programming (FLOPS 2014)　2014年6月4日

  23. 研究(分野)紹介://環境双模倣.プログラミング言語理論.理論計算機科学.計算機科学

    住井 英二郎

    日本学術会議公開シンポジウム 若手研究者ネットワーク活用に向けて: 若手研究者をめぐる諸問題へのとりくみと学際融合による研究の創出　2014年3月7日

  24. OCamlにおける多相関数の複製の実験

    徳田 亮平, 住井 英二郎

    第16回プログラミングおよびプログラミング言語ワークショップ: PPL2014　2014年3月5日

  25. λの力

    住井 英二郎

    ソフトウエアジャパン2014　2014年2月4日

  26. Environmental Bisimulation and Its Open Problems 国際会議

    Eijiro Sumii

    IFIP Working Group 2.8 31st meeting　2013年10月13日

  27. 一若手研究者（理論計算機科学）の視点

    住井 英二郎

    学術フォーラム: 社会の中の、社会のための科学技術イノベーションの推進　2013年8月7日

  28. オーダー2の高階ブーリアンプログラムの文脈等価性に関する同値類列挙

    長井 雅比古, 住井 英二郎

    第15回プログラミングおよびプログラミング言語ワークショップ: PPL2013　2013年3月4日

  29. Activities and Experiences in the Young Academy of Japan 国際会議

    Eijiro Sumii

    Microsoft Research Asia Faculty Summit 2012　2012年10月26日

  30. A Higher-Order Distributed Calculus with Name Creation

    Adrien Piérard, Eijiro Sumii

    日本ソフトウェア科学会第29回大会　2012年8月22日

  31. A Higher-Order Distributed Calculus with Name Creation 国際会議

    Adrien Piérard, Eijiro Sumii

    Twenty-Seventh Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2012)　2012年6月25日

  32. Higher Order Distribution and Name Creation 国際会議

    Adrien Piérard, Eijiro Sumii

    IFIP Working Group 2.8 29th meeting　2012年2月19日

  33. 若手研究者たちと考える、君たちの、そして日本の未来〜大学で何を学び、何をかなえたい？〜

    日本学術会議若手アカデミー委員会

    科学・技術フェスタin京都2011　2011年12月17日

  34. 環境双模倣によるプログラム等価性証明手法

    住井 英二郎

    第25回日本IBM科学賞授賞式　2011年12月1日

  35. ソフトウェア検証における計算理論的問題: 安全性検証および等価性検証の事例

    住井 英二郎

    e-サイエンスに向けた革新的アルゴリズム基盤: 第2回シンポジウム　2011年11月22日

  36. Java言語への変換によるポインタ演算の安全な実装方式

    上嶋 祐紀, 住井 英二郎

    日本ソフトウェア科学会第28回大会　2011年9月27日

  37. Report on the Fourteenth ICFP Programming Contest 国際会議

    Eijiro Sumii

    ICFP 2011: The 16th ACM SIGPLAN International Conference on Functional Programming　2011年9月19日

  38. 震災から3ヶ月半: 東北大学のこれまでと今後

    住井 英二郎

    日本学術会議公開シンポジウム 若手研究者の考える、震災後の未来: 学術に何ができるのか　2011年6月26日

  39. 高信頼・高安全ソフトウェアのための数理的検証手法：最新の研究と応用の現状

    住井 英二郎

    RSA Conference Japan 2010　2010年9月9日

  40. Parametricity via Bisimilarity (Preliminary Work) 国際会議

    Eijiro Sumii

    Dagstuhl Seminar 10351: Modelling, Controlling and Reasoning About State　2010年8月29日

  41. Environmental Bisimulations for Program Equivalence

    住井 英二郎

    第2回マイクロソフトリサーチ日本情報学研究賞授賞式　2010年7月26日

  42. Environmental Bisimulations for Program Equivalences 国際会議

    Eijiro Sumii

    IFIP Working Group 2.8 27th meeting　2010年4月11日

  43. The Higher-Order, Call-by-Value Applied Pi-Calculus 国際会議

    Nobuyuki Sato, Eijiro Sumii

    The Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)　2009年12月14日

  44. A complete characterization of observational equivalence in polymorphic lambda-calculus with general references 国際会議

    Eijiro Sumii

    Events 2009 (Max Planck Institute for Software Systems)　2009年9月10日

  45. A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References 国際会議

    Eijiro Sumii

    CSL 09: 18th EACSL Annual Conference on Computer Science Logic　2009年9月7日

  46. A Theory of Non-Monotone Memory (Or: Contexts for free) 国際会議

    Eijiro Sumii

    ESOP '09: 18th European Symposium on Programming　2009年3月25日

  47. LLで未来を発明する

    Larry Wall, まつもと ゆきひろ, 住井 英二郎, 藤田 善勝, ひげぽん

    Lightweight Language Future (LL Future)　2008年8月30日

  48. Environment Bisimulations for Higher-Order Languages 国際会議

    Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

    Scottish Programming Languages Seminar　2007年9月28日

  49. Environment Bisimulations for Higher-Order Languages 国際会議

    Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

    Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)　2007年7月10日

  50. spi計算における暗号プロトコルの形式的検証について

    住井 英二郎

    日本応用数理学会(JSIAM)「数理的技法による情報セキュリティ」研究部会(FAIS)第二回研究集会　2006年12月22日

  51. The Fail-Safe C to Java translator 国際会議

    Yuki Kamijima, Eijiro Sumii

    The Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006)　2006年11月8日

  52. ２時間で真似(まね)ぶ関数型言語のコンパイラ

    住井 英二郎

    第４回プログラミングおよびプログラミング言語サマースクール(PPL Summer School 2006)　2006年9月12日

  53. LLで関数プログラミング

    住井 英二郎, 青木 峰郎, 久井 亨, 中村 正三郎, 山下 伸夫, 今泉 貴史

    Lightweight Language Ring (LL Ring)　2006年8月26日

  54. MinCaml: a simple and efficient compiler for a minimal functional language 国際会議

    Eijiro Sumii

    Functional and Declarative Programming in Education (FDPE05)　2005年9月25日

  55. A Bisimulation for Type Abstraction and Recursion 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    The 32nd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages　2005年1月12日

  56. A Bisimulation for Type Abstraction and Recursion 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    NJPLS: The New Jersey Programming Languages and Systems Seminar Series　2004年12月3日

  57. A Bisimulation for Type Abstraction and Recursion 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    PLClub (University of Pennsylvania)　2004年10月15日

  58. A Bisimulation for Type Abstraction and Recursion 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    NEPLS: The New England Programming Languages and Systems Symposium Series　2004年10月8日

  59. セキュリティプロトコルの略式記法からspi計算への変換

    住井 英二郎, 立沢 秀晃, 米澤 明憲

    情報処理学会第48回プログラミング研究会(PRO-2003-5)　2004年3月18日

  60. 例外処理機構を備えた命令型言語のCPS変換とその定式化

    住井 英二郎, 大根田 裕一, 米澤 明憲

    情報処理学会第48回プログラミング研究会(PRO-2003-5)　2004年3月18日

  61. A Bisimulation for Dynamic Sealing

    Eijiro Sumii, Benjamin C. Pierce

    第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)　2004年3月11日

  62. A Bisimulation for Dynamic Sealing 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    The 31st Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages　2004年1月14日

  63. A Bisimulation for Dynamic Sealing 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    Dagstuhl Seminar 03411: Language-Based Security　2003年10月5日

  64. セキュリティプロトコルの略式表現からspi calculusへの変換（ショートプレゼンテーション）

    立沢 秀晃, 住井 英二郎

    第５回プログラミングおよびプログラミング言語ワークショップ(PPL2003)　2003年3月5日

  65. 例外処理機構を備えた手続き型言語のCPS変換とその定式化（ショートプレゼンテーション）

    大根田 裕一, 住井 英二郎

    第５回プログラミングおよびプログラミング言語ワークショップ(PPL2003)　2003年3月5日

  66. VMlambda: a Functional Calculus for Scientific Discovery 国際会議

    Eijiro Sumii, Hideo Bannai

    FLOPS 2002: Sixth International Symposium on Functional and Logic Programming　2002年9月15日

  67. Syntactic Logical Relations for Perfect Encryption, Higher-Order References and First-Class Channels

    住井 英二郎

    プログラミング言語セミナー（京都大学数理解析研究所）　2002年8月5日

  68. Implementing a Fail-Safe ANSI-C Compiler 国際会議

    Yutaka Oiwa, Eijiro Sumii, Akinori Yonezawa

    ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI)　2002年6月17日

  69. Safe Execution of User Programs in Kernel Mode using Typed Assembly Language 国際会議

    Toshiyuki Maeda, Eijiro Sumii, Akinori Yonezawa

    ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI)　2002年6月17日

  70. A Scheme-to-Java Translator with Soft Typing

    永田 章人, 住井 英二郎

    第5回プログラミングおよび応用のシステムに関するワークショップ: SPA '02　2002年3月4日

  71. VMλ: a Functional Calculus for Scientific Discovery 国際会議

    Eijiro Sumii, Hideo Bannai

    The Asian Workshop on Programming Languages and Systems　2001年12月17日

  72. Logical Relations for Encryption 国際会議

    Eijiro Sumii, Benjamin C. Pierce

    14th IEEE Computer Security Foundations Workshop - CSFW-14　2001年6月11日

  73. The Cryptographic λ-Calculus: Syntax, Semantics, Type System and Logical Relations

    Eijiro Sumii, Benjamin Pierce

    第3回プログラミングおよびプログラミング言語ワークショップ(PPL2001)　2001年3月21日

  74. Typed CPUおよびTyped OSのアイディア（ショートプレゼンテーション）

    住井 英二郎

    第3回プログラミングおよびプログラミング言語ワークショップ(PPL2001)　2001年3月21日

  75. Relating Cryptography and Polymorphism 国際会議

    Eijiro Sumii, Benjamin Pierce

    PLClub (University of Pennsylvania)　2000年11月3日

  76. Encoding Security Protocols in the Cryptographic lambda-Calculus 国際会議

    Eijiro Sumii, Benjamin Pierce

    PLClub (University of Pennsylvania)　2000年10月27日

  77. Relating Cryptography and Polymorphism 国際会議

    Eijiro Sumii, Benjamin Pierce

    NJPLS: The New Jersey Programming Languages and Systems Seminar Series　2000年10月24日

  78. Relating Cryptography and Polymorphism 国際会議

    Eijiro Sumii, Benjamin Pierce

    Penn Logic and Computation Seminar (University of Pennsylvania)　2000年9月25日

  79. An implementation of transparent migration on standard Scheme 国際会議

    Eijiro Sumii

    Scheme and Functional Programming 2000　2000年9月17日

  80. Online-and-Offline Partial Evaluation: A Mixed Approach 国際会議

    Eijiro Sumii, Naoki Kobayashi

    2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00)　2000年1月22日

  81. Efficient Online Partial Evaluation

    Eijiro Sumii, Naoki Kobayashi

    GPCゼミ（早稲田大学）　1999年12月13日

  82. Bridging the Gap between TDPE and SDPE

    Eijiro Sumii

    The CACA Seminar （東京大学）　1999年6月25日

  83. Online Type-Directed Partial Evaluation for Dynamically-Typed Languages

    Eijiro Sumii, Naoki Kobayashi

    第1回プログラミングおよびプログラミング言語ワークショップ(PPL'99)　1999年3月17日

  84. Linear Type Systems for Concurrent Languages 国際会議

    Eijiro Sumii

    Workshop on Linear Logic and Applications　1999年2月26日

  85. A Generalized Deadlock-Free Process Calculus 国際会議

    Eijiro Sumii, Naoki Kobayashi

    HLCL'98: 3rd International Workshop on High-Level Concurrent Languages　1998年9月12日

︎全件表示 ︎最初の5件までを表示

共同研究・競争的資金等の研究課題 14

  1. 安全・高信頼ソフトウェアシステムのための高階・型付き・並行プログラミング言語理論

    住井 英二郎

    2020年4月1日 ～ 2025年3月31日

  2. 高階・型付きの計算体系に基づくプログラミングの理論と応用の展開

    住井 英二郎

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Tohoku University

    2015年4月1日 ～ 2020年3月31日

    詳細を見る 詳細を閉じる

    主に関数型言語ないしそれに近い研究コミュニティで発展してきた，プログラミング言語理論（特に高階計算および静的型システム）をさらに発展・応用することにより，研究成果報告書の本文に列挙のとおり，多岐にわたる成果や新たな理論を得た．研究の一部は，コンピュータサイエンス分野で重要視される，水準の高い査読付国際会議にフルペーパーが採択・発表されるなど，良い評価を得た．

  3. 継続と文脈の概念にもとづく新しい関係的プログラム意味論

    住井 英二郎, 松田 一孝, キセリョーヴ オレッグ

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

    研究種目：Grant-in-Aid for Challenging Exploratory Research

    研究機関：Tohoku University

    2016年4月1日 ～ 2019年3月31日

    詳細を見る 詳細を閉じる

    「難解な専門用語の使用はできるだけ避けるか…適宜説明を加えて」「最大300文字」との指示に従って述べる。「継続」とは、計算機プログラムを実行している途中の「残りの計算」を指す概念である。「文脈」とは、プログラム中のある部分に対し、そのまわりの部分（前者を[]という記号で置き換えた、「穴」のあるプログラム）を指す。本研究では、「継続」を扱う機能の一つであるcall/ccという演算を含む関数型（式の値を計算する「評価」以外の、いわゆる「副作用」がない）プログラムの等価性（動作の等しさ）を証明するための理論を「環境双模倣」という手法にもとづき確立し、その知見を他の研究にも活かすことができた。

  4. 非単調な再帰的定義の新しい基礎理論

    住井 英二郎

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

    研究種目：Grant-in-Aid for Challenging Exploratory Research

    研究機関：Tohoku University

    2013年4月1日 ～ 2016年3月31日

    詳細を見る 詳細を閉じる

    「再帰」とは、高校で習う数列の漸化式（例えばfib(n+2) = fib(n+1) + fib(n), fib(1)=fib(2)=1と定義されるフィボナッチ数列fib）のように、定義の中に自分自身が出現するような定義のことである。再帰的定義は循環論法による矛盾が生じないよう、一定の性質（単調性）を満たす必要があり、現代的な計算機プログラミング言語の理論において本質的困難があった。本研究は新しい再帰の理論（特にプログラム等価性）により、従来は扱いが難しかった言語機能を扱えるようになった。

  5. 高階モデル検査とその応用

    小林 直樹, 篠原 歩, 五十嵐 淳, 海野 広志, 寺内 多智弘, 住井 英二郎, 松田 一孝

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (S)

    研究種目：Grant-in-Aid for Scientific Research (S)

    2011年5月31日 ～ 2016年3月31日

    詳細を見る 詳細を閉じる

    本研究の中心テーマである高階モデル検査とは、代表的なシステム検証手法であるモデル検査の拡張であり、2009年に研究代表者の小林によって初めて現実的な高階モデル検査アルゴリズムおよびプログラム検証への応用が見出された。本研究課題はその結果を受けて行った研究であり、高階モデル検査器の大幅な高速化、高階モデル検査に基づく全自動プログラム検証器の構築、高階モデル検査のデータ圧縮への応用（データをそれを生成する関数型プログラムの形に圧縮し、圧縮したままのデータ操作を実現）などの成果を得た。

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

    住井 英二郎, 寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Tohoku University

    2010年4月1日 ～ 2015年3月31日

    詳細を見る 詳細を閉じる

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

  7. ソフトウェアの安全性向上のための型理論の深化と応用

    小林 直樹, 五十嵐 淳, 住井 英二郎, 松田 一孝, 寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

    研究種目：Grant-in-Aid for Scientific Research (A)

    研究機関：Tohoku University

    2008年 ～ 2010年

    詳細を見る 詳細を閉じる

    本研究では, ソフトウェアの信頼性向上のため, これまで研究代表者らが提案してきた型に基づくプログラム検証手法を実用レベルに引き上げるとともに, 検証手法の開拓を目標としていた. 前者の主な成果として, Cプログラムやセキュリティプロトコルの自動検証ツールの構築が挙げられる. また, 後者の主な成果として, 高階モデル検査のプログラム検証への応用を示すとともに, 世界初の高階モデル検査器の構築に成功した.

  8. 順序付き線形型に基づく安全かつ高速な大規模データ処理の実現

    小林 直樹, 住井 英二郎, 西澤 弘毅

    2007年 ～ 2008年

    詳細を見る 詳細を閉じる

    XMLのような木構造を論理構造として持つテキストデータの処理の記述方式としては, その論理的構造に基づいて木構造処理として記述する方式と, 1次元のテキストデータとしての物理構造に即したストリーム処理として記述する方式がある. 本研究では,両者の長所をあわせもつ方式として、ユーザには木構造処理のプログラムを記述させ, それをストリーム処理プログラムに自動変換する方式について研究を進めている. 本年度の成果は以下のとおり。 1. XML用のストリーム処理プログラム生成器X-Pの有効性の評価 昨年度までに順序付線形型に基づくXML用のストリーム処理プログラム生成器X-Pの有効性の評価を行った. その結果, 不要なバッファリングが挿入されるケースがいくつか見つかった. 2. 順序付き非線型型を用いた一時的バッファリング 従来の変換の枠組みは, (1)木構造処理プログラムPにバッファリングを挿入することにより, 入力木に左から順に一度だけアクセスする中間プログラムIに変換し, (2)I中の木構造処理のための各命令をストリーム処理命令に置換えてストリーム処理プログラムTを得る, という2つの変換から構成されていた. (1)の変換では, Iが順序付線形型システムで型付けされるようにソースプログラムPにバッファリングを挿入することによって実現されていた. 上記1の評価で浮上した不要なバッファリングの問題は, バッファリング命令がストリームから無制限にアクセスできるメモリへのコピー命令の一種類のみであったことが主要な原因の一つであった. この問題を解決するため, 順序付き非線形型を導入することによって一時的バッファリングを実現し, 既存の木構造処理プログラムからストリーム処理プログラムへの変換の枠組みを改良した. これにより, 不要なバッファリングの問題を改善できることを実験により確認した.

  9. プログラム検証による情報保護の統一理論とその応用

    住井 英二郎

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (A)

    研究種目：Grant-in-Aid for Young Scientists (A)

    研究機関：Tohoku University

    2006年 ～ 2008年

    詳細を見る 詳細を閉じる

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

  10. ソフトウェアの安全性向上のための型理論

    小林 直樹, 住井 英二郎, 五十嵐 淳, 寺内 多智弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

    研究種目：Grant-in-Aid for Scientific Research (B)

    研究機関：Tohoku University

    2005年 ～ 2007年

    詳細を見る 詳細を閉じる

    本研究の目的は,ソフトウェアの信頼性向上のため,型理論などの数理科学的手法に基づいたプログラムの検証手法を発展させることにあった.特に,これまでの申請者らによる検証手法を改良・発展させ,現実のプログラムの検証を可能にすることに主眼をおいた. 3年間の主要な成果は以下のとおり.以下のいずれの研究においても実際にプログラム検証器のプロトタイプを作成し有効性を確認している. 1.関数型プログラムの検証手法 以前から,ファイルやメモリなどの計算資源を正しいプロトコルでアクセスするかどうかを検証するための資源使用法解析について研究を行っていたが,例外処理機構を扱っていないなど,実際のプログラミング言語とは開きがあった.そこで,従来の我々の検証手法を拡張し,例外処理機構に対応できるようにした.また,従来の型を用いた自動検証手法では,一般に解析精度が粗かったため,依存型の自動推論手法を考案することにより,精度のよい解析を自動で行えるようにした. 2.並行プログラムの検証手法 以前からπ計算を対象として,デッドロックなどの自動解析手法を研究していたが,実用化する上での解析精度,実際の言語が提供するプリミティブとの開きなどがあった.そこで,前者の問題をモデル検査などとの融合によって改善した.また,後者の問題に対処するため,ポインタや割り込みなどが入った言語に対する解析手法も考案した. 3.情報流解析 プログラムが機密情報を漏らさないかどうかを検証する情報流解析について研究を行った.従来から型を用いた情報流解析手法は提案されていたが精度が問題だったため,本研究ではモデル検査手法と融合させることにより,高速かつ精度のよい解析を可能にした.

  11. 順序付き線形型に基づく安全かつ高速な大規模データ処理の実現

    小林 直樹, 住井 英二郎

    2006年 ～ 2006年

    詳細を見る 詳細を閉じる

    本研究では,順序付き線形型理論に基づき,XML文書の木構造処理プログラムを効率のよいストリーム処理プログラムに自動変換するための枠組みの確立を目指している.本年度の成果は以下のとおり. 1.XML文書の木構造処理プログラムからストリーム処理プログラムへの自動変換の枠組みの確立 前年度までに確立していた2分木データを対象とした木構造処理プログラムからストリーム処理プログラムへの枠組みを拡張し,XML文書を対象として扱えるようにした. 2.XML用ストリーム処理プログラム生成器X-Pの試作と評価 上記1の枠組みに基づき,XML文書のための木構造処理プログラムからストリーム処理プログラムへの自動変換器X-Pを試作し,評価を行った.その結果,多くの例について1の枠組みが有効であることが確認できた.一方で,いくつかの例について,(1)無駄なバッファリング命令が挿入される,(2)文書型の情報を有効利用できていない,などの問題点が見つかった. 3.バッファリングの自動挿入の改良 ストリーム処理では,入力文書を一定の順序でしかアクセスできないため,上記1の枠組みでは,必要に応じて入力文書をバッファリングするようなストリーム処理プログラムが生成される.上記2の評価実験において,本来必要のないデータまでバッファリングされてしまう例が見つかったため,改良策として,入力木を部分的にバッファリングするための命令を追加し,自動変換の枠組みの再構築を始めた.

  12. 移動コードを基本としたセキュアなプログラミング言語処理系

    米澤 明憲, 大山 恵弘, 増原 英彦, 田浦 健次朗, 住井 英二郎, 遠藤 敏夫

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research on Priority Areas

    研究種目：Grant-in-Aid for Scientific Research on Priority Areas

    研究機関：The University of Tokyo

    2000年 ～ 2003年

    詳細を見る 詳細を閉じる

    移動コードを基本としたセキュアなプログラミング言語処理系について研究を行った。本研究では、プログラミング言語およびシステムソフトウェアの安全性にかかわる諸問題について、理論と実用の両面から研究を行った。まず、ソフトウェアの開発においてもっとも重要な要素であるプログラミング言語の様々な問題について、場当たり的な対症療法ではなく、堅固な理論にもとづく系統的な解決策を与えた。さらに、コンピュータ上でプログラムを実行する際に安全性を保証する基盤となるシステムソフトウェアに関しても、対象となるシステムへの深い理解にもとづく体系的な解決策によって問題を解決した。具体的には、C言語の安全な処理系Fail-Safe C、 Fail-Safe Cのためのインタフェース記述言語、型システムを利用して安全性を保証するOS Kernel Mode Linux、分散DoS攻撃からネットワークを守るシステムMoving Firewall、暗号ラムダ計算、文字列処理のための正規表現型、自己修復型リファレンスモニタ、プログラム部品間のアクセスをきめ細かく制御する機構、移動コードの記述を支援する言語処理系JavaGoおよびJavaGoX、Javaにおけるオブジェクト使用解析、動的型付き言語Schemeのためのリージョンベースのメモリ管理、分散計算におけるアクセス制御のための型システムなど、国内外から極めて高い評価を得ている研究実績を残した。本研究は、3つのソフトウェアの公開と30本近い査読つき論文の発表などを通じ、学術的・社会的に大きなインパクトを与え、日本ソフトウェア科学会や日経BP社から論文賞などの4つの賞を受賞した。

  13. 高性能広域分散計算のための適応的な基盤ソフトウェア

    米澤 明憲, 増原 英彦, 住井 英二郎, 田浦 健次朗, 小林 直樹, 遠藤 敏夫, 山本 泰宇, 大山 恵弘

    提供機関：Japan Society for the Promotion of Science

    制度名：Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

    研究種目：Grant-in-Aid for Scientific Research (A)

    研究機関：THE UNIVERSITY OF TOKYO

    2000年 ～ 2002年

    詳細を見る 詳細を閉じる

    本研究では、高性能なプログラム実行時処理系、とくに、実行時に判明する資源(CPU、メモリ、ネットワーク)の状況に適応して、常に良好な性能を発揮する処理系を構築することを目指した。主な成果は以下のとおりである。(1)並列言語で必要となる、共有データに対するアクセスの調停方法を、アプリケーションが持つ並列度に適応して選択し、常に良好なアクセスを行う方式を確立した(ACM PaCTに採択)。(2)分散計算において、ノードやネットワークの状況に応じて計算に参加するノードを変更できるフレームワークの設計と実装について提案を行った(ACM PPoPP, ACM/IEEE CCGridに採択)。(3)アプリケーションが必要とする計算・通信比と、与えられた資源とから、適切な(性能を最適にする)資源を選び出す問題について、アプリケーション・資源ともに性質が時間不変という仮定の下でモデル化を行い、アルゴリズムの提案とシミュレーションによる実験を行った。(4)動的なメモリ管理システムにおいて、割り当てられるメモリの局所性とメモリ使用量を自在にバランスさせることのできるメモリ管理システム方式を確立した。(5)これまで難しいとされてきた、保守的GCにおいて実時間性を確保する方式を達成した(ACM ISMMに採択)。

  14. 先進的な型システムを備えた並列/分散プログラミング言語の設計と実装

    住井 英二郎

    2000年 ～ 2000年

︎全件表示 ︎最初の5件までを表示

Works（作品等） 1

  1. MinCaml

    http://esumii.github.io/min-caml/　2005年2月 ～

    作品分類: コンピュータソフト

社会貢献活動 1

  1. 震災後「どう貢献」 若手研究者が自問自答

    2011年6月28日 ～

その他 7

  1. 静的情報保護と動的情報保護の融合のためのプログラミング言語理論

    詳細を見る 詳細を閉じる

    静的情報保護と動的情報保護の融合のためのプログラミング言語理論

  2. 第2回マイクロソフトリサーチ日本情報学研究賞（基礎的情報学分野）

    詳細を見る 詳細を閉じる

    プログラム等価性のための環境双模倣理論の構築

  3. 高階・暗号プロセス計算におけるセキュリティ検証手法

    詳細を見る 詳細を閉じる

    高階・暗号プロセス計算におけるセキュリティ検証手法

  4. プログラム等価性にもとづく高階・暗号化通信システムのセキュリティ検証手法

    詳細を見る 詳細を閉じる

    プログラム等価性にもとづく高階・暗号化通信システムのセキュリティ検証手法

  5. プログラミング言語モデルによる情報セキュリティの実現と検証

    詳細を見る 詳細を閉じる

    プログラミング言語モデルによる情報セキュリティの実現と検証

  6. MinCaml: A Simple and Efficient Compiler for a Minimal Functional Language

    詳細を見る 詳細を閉じる

    MinCaml: A Simple and Efficient Compiler for a Minimal Functional Language

  7. 美しい日本のMLコンパイラ

    詳細を見る 詳細を閉じる

    美しい日本のMLコンパイラ

︎全件表示 ︎最初の5件までを表示