TOHOKU UNIVERSITY Researchers

Details of the Researcher

Home

日本語 English

Eijiro Sumii

Section

Graduate School of Information Sciences

Job title

Professor

Degree

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

researchmap

https://researchmap.jp/read0122063

J-GLOBAL ID

200901098649003821

Research History 6

2010/11 - Present

Science Counsil of Japan　Member Member of the Young Academy of Japan, etc.
2005/05 - Present

Graduate School of Information Sciences, Tohoku University　Associate Professor (-2014), Professor (2014-)
2003/04 - 2005/03

Department of Computer and Information Science, School of Engineering and Applied Science, University of Pennsylvania　Research Associate
2001/04 - 2003/03

Interfaculty Initiative in Information Studies, University of Tokyo　Assistant Professor
2000/04 - 2001/03

日本学術振興会　特別研究員(DC1)
2000/04 - 2001/03

Department of Computer and Information Science, School of Engineering and Applied Science, University of Pennsylvania　Visiting Scholar

Show all Show first 5

Education 2

The University of Tokyo　Graduate School, Division of Science　Department of Information Science

- 2001/03
The University of Tokyo　Faculty of Science　Department of Information Science

- 1998/03

Committee Memberships 48

Journal of Functional Programming (Cambridge University Press)　Editor

2018/07 - Present
Journal of Functional Programming (Cambridge University Press)　Guest Editor

2016/09 - Present
International Federation for Information Processing (IFIP) Working Group (WG) 2.8 (Functional Programming)　Member

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

2009/04 - Present
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/06 - 2016/03
日本ソフトウェア科学会プログラミング論研究会　運営委員長

2014/04 - 2016/03
日本ソフトウェア科学会プログラミング論研究会　運営委員

2011/04 - 2016/03
Journal of Functional Programming (Cambridge University Press)　Editorial Board Member

2009/01 - 2013/12
The ACM SIGPLAN Workshop on ML　Steering Committee Chair

2010/10 - 2011/09
The ACM SIGPLAN Workshop on ML　Steering Committee Member

2008/09 - 2011/09
情報処理学会　東北支部会計幹事

2009/04 - 2011/03
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/03 - 2008/04
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/03
The 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017)　Program Committee Member

2017/01 -
21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016)　Program Chair

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

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

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

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

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

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

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

2012/09 -
Scheme 2012: Workshop on Scheme and Functional Programming　Program Committee Member

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

2012/09 -
Haskell Symposium 2012　Program Committee Member

2012/09 -
Fourteenth International Symposium on Practical Aspects of Declarative Languages: PADL'12　Program Committee Member

2012/01 -
ICFP 2011: The 16th ACM SIGPLAN International Conference on Functional Programming　Programming Contest Chair

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

2010/09 -
FLOPS 2010: Tenth International Symposium on Functional and Logic Programming　Local Chair

2010/04 -
The 2008 ACM SIGPLAN Workshop on ML　Program Chair

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

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

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

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

2007/07 -
ACM SIGPLAN Workshop on Programming Languages and Analysis for Security　Program Committee Member

2007/06 -
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/09 -
Eighth International Symposium on Functional and Logic Programming: FLOPS 2006　Program Committee Member

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

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

2005/09 -
The 2005 ACM SIGPLAN Workshop on ML　Program Committee Member

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

2005/03 -
The 2004 International Conference on Functional Programming (ICFP)　Programming Contest Organizer

2004/09 -
8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003)　Program Committee Member

2003/08 -

Show all ︎Show first 5

Professional Memberships 3

Information Processing Society of Japan
Japan Society for Software Science and Technology
Association for Computing Machinery

Research Interests 7

Pi-Calculus
Lambda-Calculus
Type Systems
Security
Functional Programming
Foundations of Software Science
Programming Language Theory

Research Areas 2

Informatics / Software /
Informatics / Information theory /

Awards 13

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

2014/02/04　情報処理学会
第9回（平成24年度）日本学術振興会賞

2013/02/04　日本学術振興会
第11回船井学術賞

2012/04/14　船井情報科学振興財団
第25回日本IBM科学賞（コンピューター・サイエンス分野）

2011/12/01　日本IBM
第1回RIEC Award東北大学研究者賞

2011/11/18　東北大学電気通信研究所
日本ソフトウェア科学会第15回論文賞

2011/06/09　日本ソフトウェア科学会
第2回マイクロソフトリサーチ日本情報学研究賞（基礎的情報学分野）

2010/07/26　マイクロソフト株式会社
第7回船井情報科学奨励賞

2008/04/19　船井情報科学振興財団
第1回野口研究奨励賞

2006/05/10　情報処理学会東北支部
2004年度上期未踏ソフトウェア創造事業天才プログラマー／スーパークリエータ

2005/05/18　情報処理推進機構
The Fifth ICFP Programming Contest (1st Place)

2002/10/05　ACM SIGPLAN International Conference on Functional Programming
日本ソフトウェア科学会第3回プログラミングおよびプログラミング言語ワークショップ論文賞

2001/02/23　日本ソフトウェア科学会
The Third Annual ICFP Programming Contest (1st Place)

2000/09/19　ACM SIGPLAN International Conference on Functional Programming

Show all ︎Show 5

Papers 67

Polymorphic Gradual Typing with Holes

KIM Jaebyeog, SUMII Eijiro

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

ISSN： 1349-3515
型システムを用いたロックフリースタックの検証

佐藤駿太朗, 住井英二郎

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

ISSN： 1349-3515
3A04 PBL Training in Freshman Orientation Camp:First-Year Experience at Dept. of Electrical, Information and Physics Engineering, Tohoku Univ.

NAKAMURA Kenji, SAITO Shin, SUMII Eijiro, WATANABE Takashi, CHEN Qiang, ITO Akinori

Proceedings of Annual Conference of Japanese Society for Engineering Education　2019　276-277　2019
Publisher: Japanese Society for Engineering Education
DOI： 10.20549/jseeja.2019.0_276 　

ISSN： 2189-8928
Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. Peer-reviewed

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
Publisher: Springer
DOI： 10.1007/978-3-030-34175-6_10 　
Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name Peer-reviewed

Masayuki Mizuno, Eijiro Sumii

Functional and Logic Programming - 14th International Symposium, FLOPS 2018, Nagoya, Japan, May 9-11, 2018, Proceedings　1-16　2018
Publisher: Springer
DOI： 10.1007/978-3-319-90686-7_1 　
Formal Verification of Functional Programs Performing Infinite Input/Output

水野雅之, 住井英二郎

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

DOI： 10.11309/jssst.34.2_114 　

ISSN： 0289-6540
A Sound and Complete Bisimulation for Contextual Equivalence in λ-Calculus with Call/cc Peer-reviewed

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 　
無限の入出力を行う関数型プログラムのK正規化の形式的検証

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

日本ソフトウェア科学会大会論文集　33　475-480　2016
Specialization of Generic Array Accesses After Inlining.

Ryohei Tokuda, Eijiro Sumii, Akinori Abe

45-53　2015

DOI： 10.4204/EPTCS.241.4 　
A Simple and Practical Linear Algebra Library Interface with Static Size Checking Peer-reviewed

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 　
Call/ccを含む型無しラムダ計算における文脈等価性の一証明手法

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

日本ソフトウェア科学会大会論文集　32　1-7　2015
A Simple and Practical Linear Algebra Library Interface with Static Size Checking Peer-reviewed

Akinori Abe, Eijiro Sumii

The OCaml Users and Developers Workshop　1-3　2014
単純かつ実用的な静的サイズ検査つき線形代数演算ライブラリ Peer-reviewed

阿部晃典, 住井英二郎

第16回プログラミングおよびプログラミング言語ワークショップ(PPL2014)論文集　1-16　2014
A Multi-Role Translation of Protocol Narration into the Spi-Calculus with Correspondence Assertions Peer-reviewed

Eijiro Sumii, Yuji Sato

FCS 2013 Workshop on Foundations of Computer Security (Informal Proceedings)　68-82　2013
対応表明つきプロトコル記述からSpiCAへの複数セッションを考慮した変換 Peer-reviewed

佐藤悠史, 住井英二郎

第15回プログラミングおよびプログラミング言語ワークショップ(PPL 2013)論文集　1-15　2013
A Higher-Order Distributed Calculus with Name Creation Peer-reviewed

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 　
From Applicative to Environmental Bisimulation Peer-reviewed

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 　
Sound Bisimulations for Higher-Order Distributed Process Calculus Peer-reviewed

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 　
Environmental bisimulations for higher-order languages Peer-reviewed

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

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

DOI： 10.1145/1889997.1890002 　

More details Close

Contains a number of typographical errors introduced by the copy editor (which the authors did not have time to correct)
Sound Bisimulations for Higher-Order Distributed Process Calculus

Adrien Piérard, Eijiro Sumii

CoRR　abs/1006.4943　1-15　2010
Limitations of Applicative Bisimulation (Preliminary Report) Invited

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
A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation Peer-reviewed

Eijiro Sumii

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

DOI： 10.1016/j.tcs.2010.09.009 　
The Higher-Order, Call-by-Value Applied Pi-Calculus Peer-reviewed

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 　
A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References Peer-reviewed

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 　
A Theory of Non-monotone Memory (Or: Contexts for free) Peer-reviewed

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 　
Java言語への変換によるポインタ演算の安全な実装方式 Peer-reviewed

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

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

DOI： 10.11309/jssst.26.1_139 　
ＭｉｎＣａｍｌコンパイラ Peer-reviewed

住井, 英二郎

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

DOI： 10.11309/jssst.25.2_28 　
A bisimulation for dynamic sealing Peer-reviewed

Eijiro Sumii, Benjamin C. Pierce

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

DOI： 10.1016/j.tcs.2006.12.032 　
Logical Bisimulations and Functional Languages Invited

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 　
Environmental Bisimulations for Higher-Order Languages Peer-reviewed

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 　
Javaへの変換による安全なC言語の実装 Peer-reviewed

上嶋祐紀, 住井英二郎

第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)論文集　52-66　2007
型安全な通信ライブラリQuicksilverとその改良 Peer-reviewed

須藤尚稔, 住井英二郎

第9回プログラミングおよびプログラミング言語ワークショップ(PPL 2007)論文集　39-51　2007
Quicksilver/OCaml: A Poor Man's Type-Safe and Abstraction-Secure Communication Library (Work in Progress)

Hisatoshi Sutou, Eijiro Sumii

Manuscript　2007
A bisimulation for type abstraction and recursion Peer-reviewed

Eijiro Sumii, Benjamin C. Pierce

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

DOI： 10.1145/1284320.1284325 　
MinCaml: a simple and efficient compiler for a minimal functional language Peer-reviewed

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 　
A bisimulation for type abstraction and recursion Peer-reviewed

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 　
A bisimulation for dynamic sealing Peer-reviewed

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 　
セキュリティプロトコルの略式記法からspi 計算への変換 Peer-reviewed

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

情報処理学会論文誌プログラミング（PRO）　45　(12)　1-10　2004
例外処理機構を備えた命令型言語のCPS変換とその定式化 Peer-reviewed

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

情報処理学会論文誌プログラミング（PRO）　45　(12)　67-82　2004
The Extension of ML with Hypothetical Views for Discovery Science: Formalization and Implementation Peer-reviewed

Eijiro Sumii, Hideo Bannai

Journal of Functional and Logic Programming　2003　1-22　2003
The Interface Definition Language for Fail-Safe C Peer-reviewed

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 　
テキスト処理言語における文字列のための正規表現型 Peer-reviewed

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

情報処理学会論文誌プログラミング（PRO）　44　(2)　1-12　2003
C++テンプレートを分割コンパイルするためのアプローチ

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

情報処理学会論文誌プログラミング（PRO）　44　(2)　42-42　2003
Fail-Safe Cのためのインターフェイス定義言語 Peer-reviewed

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

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

Eijiro Sumii, Benjamin C. Pierce

Journal of Computer Security　11　(4)　521-554　2003
Regular Expression Types for Strings in a Text Processing Language Peer-reviewed

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 　

More details Close

Errata: http://www.kb.ecei.tohoku.ac.jp/~sumii/pub/xperl.err.txt
VMλ: A Functional Calculusfor Scientific Discovery Peer-reviewed

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 　
Fail-Safe ANSI-C Compiler: An Approach to Making C Programs Secure: Progress Report Peer-reviewed

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 　
Supporting objects in run-time bytecode specialization Peer-reviewed

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 　
安全性を保証する ANSI-C 実行系の実装手法 Peer-reviewed

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

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

DOI： 10.11309/jssst.19.195 　
Linux/TAL: 型付きアセンブリプログラムのカーネルモード実行方式 Peer-reviewed

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

第4回プログラミングおよびプログラミング言語ワークショップ(PPL 2002)論文集　62-73　2002
A Scheme-to-Java Translator with Soft Typing

Akihito Nagata, Eijiro Sumii, Akinori Yonezawa

Manuscript　1-7　2002
C++テンプレートを分割コンパイルするためのアプローチ

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

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

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

第4回プログラミングおよびプログラミング言語ワークショップ(PPL 2002)論文集　74-88　2002
A Hybrid Approach to Online and Offline Partial Evaluation Peer-reviewed

Eijiro Sumii, Naoki Kobayashi

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

DOI： 10.1023/A:1012984529382 　
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
A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation Peer-reviewed

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 　
Logical Relations for Encryption Peer-reviewed

Eijiro Sumii, Benjamin C. Pierce

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

DOI： 10.1109/CSFW.2001.930151 　
The Cryptographic lambda-Calculus: Syntax, Semantics, Type System and Logical Relations Peer-reviewed

Eijiro Sumii, Benjamin C. Pierce

Informal Proceedings of the 3rd JSSST Workshop on Programming and Programming Languages (PPL 2001)　97-108　2001
安全性を保証するANSI-C実行系の実装手法

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

日本ソフトウェア科学会大会論文集　18　1-5　2001
Supporting Objects in Run-time Bytecode Specialization

Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa

日本ソフトウェア科学会大会論文集　18　1-4　2001
An Implicitly-Typed Deadlock-Free Process Calculus Peer-reviewed

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 　
Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract) Peer-reviewed

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 　
Online Type-Directed Partial Evaluation for Dynamically-Typed Languages Peer-reviewed

Eijiro Sumii, Naoki Kobayashi

Computer Software　17　(3)　230-254　2000

DOI： 10.11309/jssst.17.230 　
An Implementation of Transparent Migration on Standard Scheme Peer-reviewed

Eijiro Sumii

Proceedings of the Workshop on Scheme and Functional Programming 2000　61-63　2000
Online Type-Directed Partial Evaluation for Dynamically-Typed Languages Peer-reviewed

Eijiro Sumii, Naoki Kobayashi

Informal Proceedings of the 1st JSSST Workshop on Programming and Programming Languages (PPL 1999)　55-66　1999
A Generalized Deadlock-Free Process Calculus Peer-reviewed

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

Show all ︎Show first 5

Misc. 15

The 1st Asian National Young Academy Meeting

SUMII Eijiro

TRENDS IN THE SCIENCES　22　(9)　9_105-9_106　2017
Publisher: Japan Science Support Foundation
DOI： 10.5363/tits.22.9_105 　

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

住井, 英二郎

学術の動向 = Trends in the sciences　22　(12)　62-64　2017
私の非研究

住井, 英二郎

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

DOI： 10.11309/jssst.33.2_92 　
若手アカデミーの発足

住井, 英二郎

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

DOI： 10.5363/tits.21.3_118 　
Preface for special section from FLOPS 2014

Michael Codish, Eijiro Sumii

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

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

住井, 英二郎

情報処理　56　(5)　434-437　2015
OCaml入門：“O”が示すもの

住井英二郎

日経ソフトウエア　39-44　2014/11
Publisher: 日経BP社
特集「プログラミングおよびプログラミング言語」の編集にあたって

住井英二郎, 首藤一幸

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

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

住井, 英二郎

応用数理　17　(4)　280-290　2007
安全なC言語～プログラミング言語研究の前線から

住井英二郎

オープンソースマガジン　67-73　2006/10
Publisher: ソフトバンククリエイティブ
数理科学的バグ撲滅方法論のすすめ

住井英二郎

日経ITPro　2006/08
Publisher: 日経BP社

More details Close

第1回（2006年8月）～第16回（2007年11月）
暗号化通信のｓｐｉ計算による形式的検証

住井, 英二郎

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

DOI： 10.11309/jssst.20.607 　
TACS2001およびManfred Paul賞授賞式

五十嵐淳, 住井英二郎

情報処理　43　(2)　200-201　2002
CSFW-14報告

住井, 英二郎

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

DOI： 10.11309/jssst.18.637 　
POPL/PEPM'99会議報告

住井英二郎, 小林直樹

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

Show all ︎Show first 5

Books and Other Publications 6

プログラム意味論の基礎

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

サイエンス社　2020/08

ISBN: 9784781914831
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
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
TYPES AND PROGRAMMING LANGUAGES

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

オーム社　2013

ISBN: 9784274069116
数理的技法による情報セキュリティ

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

共立出版　2010

ISBN: 9784320019508
Proceedings of the ACM Workshop on ML, 2008, Victoria, BC, Canada, September 21, 2008

Eijiro Sumii

ACM　2008

ISBN: 9781605580623

Show all Show first 5

Presentations 85

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

続隼人, 住井英二郎

第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）　2025/03/07
セキュリティ束の動的拡張が可能なπ計算の型ベース情報流解析

織田幸弘, 住井英二郎

第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）　2025/03/06
RustへのFractional Ownershipの動的検査の導入

馬場風汰, 住井英二郎

第26回プログラミングおよびプログラミング言語ワークショップ（PPL 2024）　2024/03/06
構造化グラフの正規化の証明

柳沢大貴, 住井英二郎

第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023/03
複数参加者非同期セッション型の一般プロセス型への変換

細川万里奈, 住井英二郎

第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023/03
LEGO Education SPIKE PrimeのMicroPython環境における関数型リアクティブプログラミング

中里匡亮, 住井英二郎

第25回プログラミングおよびプログラミング言語ワークショップ（PPL 2023）　2023/03
定理証明支援器Coqを用いた計算量の証明の改良

中村悠紀, 住井英二郎

PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021/03/10
MetaOCamlによる自律型ロボットのためのCコード生成

山本うらん, 住井英二郎

PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021/03/10
SMTソルバーを利用した算術式を含む高階関数の等価性検証手法

遠藤瑛輔, 住井英二郎

PPL 2021: 第23回プログラミングおよびプログラミング言語ワークショップ　2021/03/09
Progress report: Ruby 3における静的型解析の実現に向けて

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

第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019/03/06
ブロックチェーン合意形成プロトコルのCoqによる証明からのコード抽出

木村朝輝, 住井英二郎

第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019/03/06
NetKAT with Cryptography

菅原慎之介, 住井英二郎

第21回プログラミングおよびプログラミング言語ワークショップ（PPL2019）　2019/03/06
Experiences in the Young Academy of Japan International-presentation

Eijiro Sumii

2017 Y-KAST - YAJ Bilateral Workshop on "Institutional and Scientific Challenges for Young Scientists in Asia"　2017/03/15
Established NYAs in Asia: Success Story and Initiatives International-presentation

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
Program Chair Report International-presentation

Eijiro Sumii

ICFP 2016: The 21st ACM SIGPLAN International Conference on Functional Programming　2016/09/18
機械学習による関数型ブーリアンプログラムの型推論

阿部晃典, 住井英二郎

第18回プログラミングおよびプログラミング言語ワークショップ（PPL2016）　2016/03/07
プログラムの論理

住井英二郎

第61回情報科学談話会　2015/12/03
Global Young Academy: The voice of young scientists around the world International-presentation

Eijiro Sumii

The Third UN World Conference on Disaster Risk Reduction, Science and Technology Major Group Booth　2015/03/17
An Experiment for Duplication of Polymorphic Functions in OCaml International-presentation

Ryohei Tokuda, Eijiro Sumii

APLAS 2014: 12th Asian Symposium on Programming Languages and Systems　2014/11/17
Normalizing Structured Graphs International-presentation

Eijiro Sumii, Kazuma Kikuchi

IFIP Working Group 2.8 32nd meeting　2014/08/11
いわゆる「情報系」研究者・技術者のキャリアパスについて

住井英二郎

筑波大学附属駒場高等学校進路懇談会　2014/07/05
Opening International-presentation

Eijiro Sumii

Twelfth International Symposium on Functional and Logic Programming (FLOPS 2014)　2014/06/04
研究(分野)紹介://環境双模倣.プログラミング言語理論.理論計算機科学.計算機科学

住井英二郎

日本学術会議公開シンポジウム若手研究者ネットワーク活用に向けて: 若手研究者をめぐる諸問題へのとりくみと学際融合による研究の創出　2014/03/07
OCamlにおける多相関数の複製の実験

徳田亮平, 住井英二郎

第16回プログラミングおよびプログラミング言語ワークショップ: PPL2014　2014/03/05
λの力

住井英二郎

ソフトウエアジャパン2014　2014/02/04
Environmental Bisimulation and Its Open Problems International-presentation

Eijiro Sumii

IFIP Working Group 2.8 31st meeting　2013/10/13
一若手研究者（理論計算機科学）の視点

住井英二郎

学術フォーラム: 社会の中の、社会のための科学技術イノベーションの推進　2013/08/07
オーダー2の高階ブーリアンプログラムの文脈等価性に関する同値類列挙

長井雅比古, 住井英二郎

第15回プログラミングおよびプログラミング言語ワークショップ: PPL2013　2013/03/04
Activities and Experiences in the Young Academy of Japan International-presentation

Eijiro Sumii

Microsoft Research Asia Faculty Summit 2012　2012/10/26
A Higher-Order Distributed Calculus with Name Creation

Adrien Piérard, Eijiro Sumii

日本ソフトウェア科学会第29回大会　2012/08/22
A Higher-Order Distributed Calculus with Name Creation International-presentation

Adrien Piérard, Eijiro Sumii

Twenty-Seventh Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS 2012)　2012/06/25
Higher Order Distribution and Name Creation International-presentation

Adrien Piérard, Eijiro Sumii

IFIP Working Group 2.8 29th meeting　2012/02/19
若手研究者たちと考える、君たちの、そして日本の未来〜大学で何を学び、何をかなえたい？〜

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

科学・技術フェスタin京都2011　2011/12/17
環境双模倣によるプログラム等価性証明手法

住井英二郎

第25回日本IBM科学賞授賞式　2011/12/01
ソフトウェア検証における計算理論的問題: 安全性検証および等価性検証の事例

住井英二郎

e-サイエンスに向けた革新的アルゴリズム基盤: 第2回シンポジウム　2011/11/22
Java言語への変換によるポインタ演算の安全な実装方式

上嶋祐紀, 住井英二郎

日本ソフトウェア科学会第28回大会　2011/09/27
Report on the Fourteenth ICFP Programming Contest International-presentation

Eijiro Sumii

ICFP 2011: The 16th ACM SIGPLAN International Conference on Functional Programming　2011/09/19
震災から3ヶ月半: 東北大学のこれまでと今後

住井英二郎

日本学術会議公開シンポジウム若手研究者の考える、震災後の未来: 学術に何ができるのか　2011/06/26
高信頼・高安全ソフトウェアのための数理的検証手法：最新の研究と応用の現状

住井英二郎

RSA Conference Japan 2010　2010/09/09
Parametricity via Bisimilarity (Preliminary Work) International-presentation

Eijiro Sumii

Dagstuhl Seminar 10351: Modelling, Controlling and Reasoning About State　2010/08/29
Environmental Bisimulations for Program Equivalence

住井英二郎

第2回マイクロソフトリサーチ日本情報学研究賞授賞式　2010/07/26
Environmental Bisimulations for Program Equivalences International-presentation

Eijiro Sumii

IFIP Working Group 2.8 27th meeting　2010/04/11
The Higher-Order, Call-by-Value Applied Pi-Calculus International-presentation

Nobuyuki Sato, Eijiro Sumii

The Seventh Asian Symposium on Programming Languages and Systems (APLAS 2009)　2009/12/14
A complete characterization of observational equivalence in polymorphic lambda-calculus with general references International-presentation

Eijiro Sumii

Events 2009 (Max Planck Institute for Software Systems)　2009/09/10
A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References International-presentation

Eijiro Sumii

CSL 09: 18th EACSL Annual Conference on Computer Science Logic　2009/09/07
A Theory of Non-Monotone Memory (Or: Contexts for free) International-presentation

Eijiro Sumii

ESOP '09: 18th European Symposium on Programming　2009/03/25
LLで未来を発明する

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

Lightweight Language Future (LL Future)　2008/08/30
Environment Bisimulations for Higher-Order Languages International-presentation

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

Scottish Programming Languages Seminar　2007/09/28
Environment Bisimulations for Higher-Order Languages International-presentation

Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii

Twenty-Second Annual IEEE Symposium on Logic in Computer Science (LICS 2007)　2007/07/10
spi計算における暗号プロトコルの形式的検証について

住井英二郎

日本応用数理学会(JSIAM)「数理的技法による情報セキュリティ」研究部会(FAIS)第二回研究集会　2006/12/22
The Fail-Safe C to Java translator International-presentation

Yuki Kamijima, Eijiro Sumii

The Fourth ASIAN Symposium on Programming Languages and Systems (APLAS 2006)　2006/11/08
２時間で真似(まね)ぶ関数型言語のコンパイラ

住井英二郎

第４回プログラミングおよびプログラミング言語サマースクール(PPL Summer School 2006)　2006/09/12
LLで関数プログラミング

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

Lightweight Language Ring (LL Ring)　2006/08/26
MinCaml: a simple and efficient compiler for a minimal functional language International-presentation

Eijiro Sumii

Functional and Declarative Programming in Education (FDPE05)　2005/09/25
A Bisimulation for Type Abstraction and Recursion International-presentation

Eijiro Sumii, Benjamin C. Pierce

The 32nd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages　2005/01/12
A Bisimulation for Type Abstraction and Recursion International-presentation

Eijiro Sumii, Benjamin C. Pierce

NJPLS: The New Jersey Programming Languages and Systems Seminar Series　2004/12/03
A Bisimulation for Type Abstraction and Recursion International-presentation

Eijiro Sumii, Benjamin C. Pierce

PLClub (University of Pennsylvania)　2004/10/15
A Bisimulation for Type Abstraction and Recursion International-presentation

Eijiro Sumii, Benjamin C. Pierce

NEPLS: The New England Programming Languages and Systems Symposium Series　2004/10/08
セキュリティプロトコルの略式記法からspi計算への変換

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

情報処理学会第48回プログラミング研究会(PRO-2003-5)　2004/03/18
例外処理機構を備えた命令型言語のCPS変換とその定式化

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

情報処理学会第48回プログラミング研究会(PRO-2003-5)　2004/03/18
A Bisimulation for Dynamic Sealing

Eijiro Sumii, Benjamin C. Pierce

第6回プログラミングおよびプログラミング言語ワークショップ(PPL2004)　2004/03/11
A Bisimulation for Dynamic Sealing International-presentation

Eijiro Sumii, Benjamin C. Pierce

The 31st Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages　2004/01/14
A Bisimulation for Dynamic Sealing International-presentation

Eijiro Sumii, Benjamin C. Pierce

Dagstuhl Seminar 03411: Language-Based Security　2003/10/05
セキュリティプロトコルの略式表現からspi calculusへの変換（ショートプレゼンテーション）

立沢秀晃, 住井英二郎

第５回プログラミングおよびプログラミング言語ワークショップ(PPL2003)　2003/03/05
例外処理機構を備えた手続き型言語のCPS変換とその定式化（ショートプレゼンテーション）

大根田裕一, 住井英二郎

第５回プログラミングおよびプログラミング言語ワークショップ(PPL2003)　2003/03/05
VMlambda: a Functional Calculus for Scientific Discovery International-presentation

Eijiro Sumii, Hideo Bannai

FLOPS 2002: Sixth International Symposium on Functional and Logic Programming　2002/09/15
Syntactic Logical Relations for Perfect Encryption, Higher-Order References and First-Class Channels

住井英二郎

プログラミング言語セミナー（京都大学数理解析研究所）　2002/08/05
Implementing a Fail-Safe ANSI-C Compiler International-presentation

Yutaka Oiwa, Eijiro Sumii, Akinori Yonezawa

ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI)　2002/06/17
Safe Execution of User Programs in Kernel Mode using Typed Assembly Language International-presentation

Toshiyuki Maeda, Eijiro Sumii, Akinori Yonezawa

ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI)　2002/06/17
A Scheme-to-Java Translator with Soft Typing

永田章人, 住井英二郎

第5回プログラミングおよび応用のシステムに関するワークショップ: SPA '02　2002/03/04
VMλ: a Functional Calculus for Scientific Discovery International-presentation

Eijiro Sumii, Hideo Bannai

The Asian Workshop on Programming Languages and Systems　2001/12/17
Logical Relations for Encryption International-presentation

Eijiro Sumii, Benjamin C. Pierce

14th IEEE Computer Security Foundations Workshop - CSFW-14　2001/06/11
The Cryptographic λ-Calculus: Syntax, Semantics, Type System and Logical Relations

Eijiro Sumii, Benjamin Pierce

第3回プログラミングおよびプログラミング言語ワークショップ(PPL2001)　2001/03/21
Typed CPUおよびTyped OSのアイディア（ショートプレゼンテーション）

住井英二郎

第3回プログラミングおよびプログラミング言語ワークショップ(PPL2001)　2001/03/21
Relating Cryptography and Polymorphism International-presentation

Eijiro Sumii, Benjamin Pierce

PLClub (University of Pennsylvania)　2000/11/03
Encoding Security Protocols in the Cryptographic lambda-Calculus International-presentation

Eijiro Sumii, Benjamin Pierce

PLClub (University of Pennsylvania)　2000/10/27
Relating Cryptography and Polymorphism International-presentation

Eijiro Sumii, Benjamin Pierce

NJPLS: The New Jersey Programming Languages and Systems Seminar Series　2000/10/24
Relating Cryptography and Polymorphism International-presentation

Eijiro Sumii, Benjamin Pierce

Penn Logic and Computation Seminar (University of Pennsylvania)　2000/09/25
An implementation of transparent migration on standard Scheme International-presentation

Eijiro Sumii

Scheme and Functional Programming 2000　2000/09/17
Online-and-Offline Partial Evaluation: A Mixed Approach International-presentation

Eijiro Sumii, Naoki Kobayashi

2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00)　2000/01/22
Efficient Online Partial Evaluation

Eijiro Sumii, Naoki Kobayashi

GPCゼミ（早稲田大学）　1999/12/13
Bridging the Gap between TDPE and SDPE

Eijiro Sumii

The CACA Seminar （東京大学）　1999/06/25
Online Type-Directed Partial Evaluation for Dynamically-Typed Languages

Eijiro Sumii, Naoki Kobayashi

第1回プログラミングおよびプログラミング言語ワークショップ(PPL'99)　1999/03/17
Linear Type Systems for Concurrent Languages International-presentation

Eijiro Sumii

Workshop on Linear Logic and Applications　1999/02/26
A Generalized Deadlock-Free Process Calculus International-presentation

Eijiro Sumii, Naoki Kobayashi

HLCL'98: 3rd International Workshop on High-Level Concurrent Languages　1998/09/12

Show all Show first 5

Research Projects 14

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

住井英二郎

Offer Organization: 日本学術振興会

System: 科学研究費助成事業基盤研究(B)

Category: 基盤研究(B)

Institution: 東北大学

2020/04/01 - 2025/03/31
Development of theory and application of programming based on higher-order/typed calculi

Sumii Eijiro

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

Category: Grant-in-Aid for Scientific Research (B)

Institution: Tohoku University

2015/04/01 - 2020/03/31

More details Close

As enumerated in the report, a variety of results and new theories have been obtained by developing and applying programming language theory (in particular, higher-order computation and static type systems) studied in functional languages and related research fields. Some of our research has been accepted as full papers and presented in refereed, high-quality international conferences.
New reational program semantics based on the notion of continuations and contexts

Sumii Eijiro, Matsuda Kazutaka, Kiselyov Oleg

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

Category: Grant-in-Aid for Challenging Exploratory Research

Institution: Tohoku University

2016/04/01 - 2019/03/31

More details Close

A theory for proving program equivalence, based on environmental bisimulations, has been developed in a foundational calculus modelling a functional programming language with the undelimited continuation operator "call/cc" (call-with-current-continuation).
Studies for Non-Monotone Recursion

SUMII Eijiro

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Challenging Exploratory Research

Category: Grant-in-Aid for Challenging Exploratory Research

Institution: Tohoku University

2013/04/01 - 2016/03/31

More details Close

We studied a new theory of recursion (for program equivalence, in particular) for programs and programming languages with advanced features such as graphs and first-class continuations.
Higher-Order Model Checking and its Applications

Kobayashi Naoki, SHINOHARA Ayumi, IGARASHI Atsushi, UNNO Hiroshi, TERAUCHI Tachio, SUMII Eijiro, MATSUDA Kazutaka

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (S)

Category: Grant-in-Aid for Scientific Research (S)

2011/05/31 - 2016/03/31

More details Close

The main topic of this research project was higher-order model checking, which is an extension of model checking, a representative method for system verification. In 2009, Kobayashi, the leader of this project, has developed the first practical algorithm for higher-order model checking, and also shown that higher-order model checking is useful for program verification. This research project has been launched to extend his results. The major results include: the development of much faster higher-order model checkers, implementation of fully-automated tools for program verification, and applications to data compression (where data are compressed in the form of functional programs that generate them, and compressed data are manipulated without decompression).
Formal Verification of Higher-Order Open Systems

SUMII Eijiro, TERAUCHI Tachio

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

Category: Grant-in-Aid for Scientific Research (B)

Institution: Tohoku University

2010/04/01 - 2015/03/31

More details Close

We developed the first sound and complete theory for proving behavioral equivalence ("makes the same actions" when observed externally) in higher-order (processes themselves can be communicated), concurrent and distributed ("has the notion of locations") computation model (process calculus), and published the results in refereed venues such as LICS 2012, a top conference on theoretical computer science.
Advancement and Application of Type Theory for Improving Software Safety

KOBAYASHI Naoki, IGARASHI Atsushi, SUMII Eijiro, MATSUDA Kazutaka, TERAUCHI Tachio

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

Category: Grant-in-Aid for Scientific Research (A)

Institution: Tohoku University

2008 - 2010

More details Close

This research project aimed to improve the reliability of computer software, by refining type-based program verification methods we have studied before, and also by inventing new program verification techniques. As the former study, we have constructed verification tools for C programs and cryptographic protocols. As the latter study, we have shown novel applications of higher-order model checking to program verification, and constructed the first higher-order model checker in the world.
順序付き線形型に基づく安全かつ高速な大規模データ処理の実現

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

Offer Organization: 日本学術振興会

System: 科学研究費助成事業特定領域研究

Category: 特定領域研究

Institution: 東北大学

2007 - 2008

More details Close

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

SUMII Eijiro

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (A)

Category: Grant-in-Aid for Young Scientists (A)

Institution: Tohoku University

2006 - 2008
Type Theory for Software Safety

KOBAYSHI Naoki, SUMII Eijiro, IGARASHI Atsushi, TERAUCHI Tachio

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (B)

Category: Grant-in-Aid for Scientific Research (B)

Institution: Tohoku University

2005 - 2007

More details Close

The purpose of this project was to enhance software verification techniques based on formal methods such as type theories. The primary goal was to refine and extend our previous type-based verification techniques so that they can be used for verification of realistic programs. The main results are summarized as follows. For each topic, we have implemented a prototype verification system and confirmed the effectiveness of the verification technique. 1. Verification methods for functional programs A main shortcoming of our previous type-based technique for resource usage verification was that it did not properly handle advanced language mechanisms such as exceptions. We have extended the previous resource usage verification technique to deal with exceptions. We have also devised an (incomplete) algorithm to infer dependent types, to enable automatic but more precise program analysis than previous methods. 2. Verification methods for concurrent programs The main shortcomings of our previous verification method were that it was too imprecise and that it did not handle some common primitives such as reference cells and interrupts. To address the former issue, we have integrated our previous type-based method with model-checking techniques. For the latter issue, we have developed verification methods for a C-like language with interrupts and reference cells. 3. Information Flow Analysis We have integrated a type-based technique for information flow analysis with a mode-checking technique. The resulting analysis is more precise than previous type-based techniques, and more efficient than previous model-checking techniques for information flow analysis.
順序付き線形型に基づく安全かつ高速な大規模データ処理の実現

小林直樹, 住井英二郎

Offer Organization: 日本学術振興会

System: 科学研究費助成事業特定領域研究

Category: 特定領域研究

Institution: 東北大学

2006 - 2006

More details Close

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

YONEZAWA Akinori, OYAMA Yoshihiro, MASUHARA Hidehiko, TAURA Kenjiro

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research on Priority Areas

Category: Grant-in-Aid for Scientific Research on Priority Areas

Institution: The University of Tokyo

2000 - 2003

More details Close

We studied secure programming languages based on mobile code. We worked on essential research issues in security of programming languages and system software from both theoretical and practical aspects. First we gave a systematic solution to problems in programming languages, which is the most important element in software development. The solution is not ad-hoc but based on a solid theory. Furthermore, we addressed research issues in system software with a systematic solution based on deep understanding of target systems. The results of this research include a secure compiler for the C programming language (Fail-Safe C), an interface definition language for Fail-Safe C, an operating system that guarantees security using type systems (Kernel Mode Linux), a system that defends networks against distributed denial of service attacks (MovingFirewall), cryptographic lambda calculus, regular expression types for string operations, self-repairing reference monitors, a fine-grain access control mechanism between program modules, programming languages that support the description of mobile code (JavaGO and JavaGoX), object usage analysis for Java, efficient regjon-based memory management for a dynamical ly-typed programming language Scheme, and a type system for access control in distributed computation. The results are highly evaluated by internat ional communit of computer science. This research had a significant impact on academic and industrial fields by releasing three software and publishing about 30 refereed papers. We received four prestigious awards including the best paper award from Japan Society for Software Science and the best technology award from Nikkei Business Publications Inc.
Adaptive Software Substrate for High Performance Wide Area Computing

YONEZAWA Akinori, MASUHARA Hidehiko, SUMII Eijirou, TAURA Kenjirou, KOBAYASHI Naoki

Offer Organization: Japan Society for the Promotion of Science

System: Grants-in-Aid for Scientific Research Grant-in-Aid for Scientific Research (A)

Category: Grant-in-Aid for Scientific Research (A)

Institution: THE UNIVERSITY OF TOKYO

2000 - 2002

More details Close

The objective of this project was to establish foundations for building adaptive runtime systems, which behave well under various resource conditions (of CPU, memory, and network) that reveal at runtime. Main results are as follows, (1) We established an efficient access control (e.g., mutual exclusion) method for shared data, which adapts to the degree of parallelism in the application (published in ACM PaCT). (2) We proposed a framework in which parallel applications can migrate from a set of resources to another at runtime, depending on resource conditions (published or to be published in ACM PPoPP and ACM/IEEE CCGrid). (3) We tackled the resource selection problem in which the system, given computation/communication requirements of the application and computation/communication capacity of available resources, tries to select good resources for the application automatically. It proposed the problem formulation, an algorithm assuming resource requirements and conditions do not change over time, and conducted a simulation. (4) We established a dynamic memory management scheme that can trade thread-level locality of allocated memory and the total memory requirements. (5) We achieved a very short pause time (less than 10ms) for conservative garbage collectors, which have been considered to be difficult in the community (published in ACM ISMM).
先進的な型システムを備えた並列/分散プログラミング言語の設計と実装

住井英二郎

Offer Organization: 日本学術振興会

System: 科学研究費助成事業特別研究員奨励費

Category: 特別研究員奨励費

Institution: 東京大学

2000 - 2000

Show all Show first 5

Works 1

MinCaml

http://esumii.github.io/min-caml/ 2005/02 -

Type: Software

Social Activities 1

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

2011/06/28 -

Other 7

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

More details Close

静的情報保護と動的情報保護の融合のためのプログラミング言語理論
第2回マイクロソフトリサーチ日本情報学研究賞（基礎的情報学分野）

More details Close

プログラム等価性のための環境双模倣理論の構築
高階・暗号プロセス計算におけるセキュリティ検証手法

More details Close

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

More details Close

プログラム等価性にもとづく高階・暗号化通信システムのセキュリティ検証手法
プログラミング言語モデルによる情報セキュリティの実現と検証

More details Close

プログラミング言語モデルによる情報セキュリティの実現と検証
MinCaml: A Simple and Efficient Compiler for a Minimal Functional Language

More details Close

MinCaml: A Simple and Efficient Compiler for a Minimal Functional Language
美しい日本のMLコンパイラ

More details Close

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

Show all Show first 5