| 2016 | FM | Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. | Hanno Becker, Juan Manuel Crespo, Jacek Galowicz, Ulrich Hensel, Yoichi Hirai, Csar Kunz, Keiko Nakata, Jorge Luis Sacchini, Hendrik Tews, Thomas Tuerk |
| 2015 | TABLEAUX | A Dynamic Logic with Traces and Coinduction. | Richard Bubel, Crystal Chang Din, Reiner Hhnle, Keiko Nakata |
| 2013 | ICALP | Contractive Signatures with Recursive Types, Type Parameters, and Abstract Types. | Hyeonseung Im, Keiko Nakata, Sungwoo Park |
| 2012 | FLOPS | Classical Call-by-Need Sequent Calculi: The Unity of Semantic Artifacts. | Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, Alexis Saurin |
| 2011 | APLAS | A Proof Pearl with the Fan Theorem and Bar Induction - Walking through Infinite Trees with Mixed Induction and Coinduction. | Keiko Nakata, Tarmo Uustalu, Marc Bezem |
| 2011 | OOPSLA | A syntactic type system for recursive modules. | Hyeonseung Im, Keiko Nakata, Jacques Garrigue, Sungwoo Park |
| 2010 | ESOP | A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While. | Keiko Nakata, Tarmo Uustalu |
| 2006 | ICFP | Recursive modules for programming. | Keiko Nakata, Jacques Garrigue |
| 1993 | ICTAI | Advantages of Meta-Level Control Architectures in Maintaining Rule-Based Systems. | Yutaka Sasaki, Keiko Nakata, Toru Ishida, Yoshimi Fukuhara |