A Generalized Deadlock-Free Process Calculus. - Eijiro Sumii; Naoki Kobayashi 001 (HLCL, 1998)

An Implicitly-Typed Deadlock-Free Process Calculus. - Naoki Kobayashi 001; Shin Saito; Eijiro Sumii (CONCUR, 2000)

Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract). - Eijiro Sumii; Naoki Kobayashi 001 (PEPM, 2000)

VM lambda: a Functional Calculus for Scientific Discovery. - Eijiro Sumii; Hideo Bannai (APLAS, 2001)

A Typed Process Calculus for Fine-Grained Resource Access Control in Distributed Computation. - Daisuke Hoshina; Eijiro Sumii; Akinori Yonezawa (TACS, 2001)

A Hybrid Approach to Online and Offline Partial Evaluation. - Eijiro Sumii; Naoki Kobayashi 001 (High. Order Symb. Comput., 2001)

VM lambda: A Functional Calculusfor Scientific Discovery. - Eijiro Sumii; Hideo Bannai (FLOPS, 2002)

Fail-Safe ANSI-C Compiler: An Approach to Making C Programs Secure: Progress Report. - Yutaka Oiwa; Tatsurou Sekiguchi; Eijiro Sumii; Akinori Yonezawa (ISSS, 2002)

Supporting objects in run-time bytecode specialization. - Reynald Affeldt; Hidehiko Masuhara; Eijiro Sumii; Akinori Yonezawa (ASIA-PEPM, 2002)

Regular Expression Types for Strings in a Text Processing Language. - Naoshi Tabuchi; Eijiro Sumii; Akinori Yonezawa (TIP@MPC, 2002)

The Interface Definition Language for Fail-Safe C. - Kohei Suenaga; Yutaka Oiwa; Eijiro Sumii; Akinori Yonezawa (ISSS, 2003)

Logical Relations for Encryption. - Eijiro Sumii; Benjamin C. Pierce (J. Comput. Secur., 2003)

The Extension of ML with Hypothetical Views for Discovery Science: Formalization and Implementation. - Eijiro Sumii; Hideo Bannai (J. Funct. Log. Program., 2003)

MinCaml: a simple and efficient compiler for a minimal functional language. - Eijiro Sumii (FDPE@ICFP, 2005)

Logical Bisimulations and Functional Languages. - Davide Sangiorgi; Naoki Kobayashi 001; Eijiro Sumii (FSEN, 2007)

A bisimulation for type abstraction and recursion. - Eijiro Sumii; Benjamin C. Pierce (J. ACM, 2007)

A bisimulation for dynamic sealing. - Eijiro Sumii; Benjamin C. Pierce (Theor. Comput. Sci., 2007)

The Higher-Order, Call-by-Value Applied Pi-Calculus. - Nobuyuki Sato; Eijiro Sumii (APLAS, 2009)

A Complete Characterization of Observational Equivalence in Polymorphic lambda-Calculus with General References. - Eijiro Sumii (CSL, 2009)

A Theory of Non-monotone Memory (Or: Contexts for free). - Eijiro Sumii (ESOP, 2009)

Limitations of Applicative Bisimulation (Preliminary Report). - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (Modelling, Controlling and Reasoning About State, 2010)

A bisimulation-like proof method for contextual properties in untyped lambda-calculus with references and deallocation. - Eijiro Sumii (Theor. Comput. Sci., 2010)

Sound Bisimulations for Higher-Order Distributed Process Calculus. - Adrien Piérard; Eijiro Sumii (FoSSaCS, 2011)

From Applicative to Environmental Bisimulation. - Vasileios Koutavas; Paul Blain Levy; Eijiro Sumii (MFPS, 2011)

Environmental bisimulations for higher-order languages. - Davide Sangiorgi; Naoki Kobayashi 001; Eijiro Sumii (ACM Trans. Program. Lang. Syst., 2011)

A Higher-Order Distributed Calculus with Name Creation. - Adrien Piérard; Eijiro Sumii (LICS, 2012)

A Simple and Practical Linear Algebra Library Interface with Static Size Checking. - Akinori Abe; Eijiro Sumii (ML/OCaml, 2014)

Specialization of Generic Array Accesses After Inlining. - Ryohei Tokuda; Eijiro Sumii; Akinori Abe (ML Family/OCaml, 2015)

A Sound and Complete Bisimulation for Contextual Equivalence in lambda -Calculus with Call/cc. - Taichi Yachi; Eijiro Sumii (APLAS, 2016)

Preface for special section from FLOPS 2014. - Michael Codish; Eijiro Sumii (J. Funct. Program., 2016)

Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name. - Masayuki Mizuno; Eijiro Sumii (FLOPS, 2018)

Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. - Masayuki Mizuno; Eijiro Sumii (APLAS, 2019)