| 2019 | APLAS | Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. | Masayuki Mizuno, Eijiro Sumii |
| 2018 | FLOPS | Formal Verification of the Correspondence Between Call-by-Need and Call-by-Name. | Masayuki Mizuno, Eijiro Sumii |
| 2016 | APLAS | A Sound and Complete Bisimulation for Contextual Equivalence in \lambda -Calculus with Call/cc. | Taichi Yachi, Eijiro Sumii |
| 2012 | LICS | A Higher-Order Distributed Calculus with Name Creation. | Adrien Pirard, Eijiro Sumii |
| 2011 | FOSSACS | Sound Bisimulations for Higher-Order Distributed Process Calculus. | Adrien Pirard, Eijiro Sumii |
| 2009 | APLAS | The Higher-Order, Call-by-Value Applied Pi-Calculus. | Nobuyuki Sato, Eijiro Sumii |
| 2009 | CSL | A Complete Characterization of Observational Equivalence in Polymorphic | Eijiro Sumii |
| 2009 | ESOP | A Theory of Non-monotone Memory (Or: Contexts for free). | Eijiro Sumii |
| 2007 | LICS | Environmental Bisimulations for Higher-Order Languages. | Davide Sangiorgi, Naoki Kobayashi, Eijiro Sumii |
| 2005 | ICFP | MinCaml: a simple and efficient compiler for a minimal functional language. | Eijiro Sumii |
| 2005 | POPL | A bisimulation for type abstraction and recursion. | Eijiro Sumii, Benjamin C. Pierce |
| 2004 | POPL | A bisimulation for dynamic sealing. | Eijiro Sumii, Benjamin C. Pierce |
| 2002 | FLOPS | VM lambda: A Functional Calculusfor Scientific Discovery. | Eijiro Sumii, Hideo Bannai |
| 2002 | PEPM | Supporting objects in run-time bytecode specialization. | Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa |
| 2001 | APLAS | VM lambda: a Functional Calculus for Scientific Discovery. | Eijiro Sumii, Hideo Bannai |
| 2000 | CONCUR | An Implicitly-Typed Deadlock-Free Process Calculus. | Naoki Kobayashi, Shin Saito, Eijiro Sumii |
| 2000 | PEPM | Online-and-Offline Partial Evaluation: A Mixed Approach (Extended Abstract). | Eijiro Sumii, Naoki Kobayashi |