| 2024 | FSCD | Representation of Peano Arithmetic in Separation Logic. | Sohei Ito, Makoto Tatsuta |
| 2021 | APLAS | Function Pointer Eliminator for C Programs. | Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa |
| 2019 | APLAS | Completeness of Cyclic Proofs for Symbolic Heaps with Inductive Definitions. | Makoto Tatsuta, Koji Nakazawa, Daisuke Kimura |
| 2017 | APLAS | Decision Procedure for Entailment of Symbolic Heaps with Arrays. | Daisuke Kimura, Makoto Tatsuta |
| 2017 | CAV | A Decidable Fragment in Separation Logic with Inductive Predicates and Arithmetic. | Quang Loc Le, Makoto Tatsuta, Jun Sun, Wei-Ngan Chin |
| 2017 | FOSSACS | Classical System of Martin-Lf's Inductive Definitions Is Not Equivalent to Cyclic Proof System. | Stefano Berardi, Makoto Tatsuta |
| 2017 | LICS | Equivalence of inductive definitions and cyclic proofs under arithmetic. | Stefano Berardi, Makoto Tatsuta |
| 2016 | APLAS | Decision Procedure for Separation Logic with Inductive Definitions and Presburger Arithmetic. | Makoto Tatsuta, Quang Loc Le, Wei-Ngan Chin |
| 2015 | APLAS | Separation Logic with Monadic Inductive Definitions and Implicit Existentials. | Makoto Tatsuta, Daisuke Kimura |
| 2014 | SEFM | Completeness of Separation Logic with Inductive Definitions for Program Verification. | Makoto Tatsuta, Wei-Ngan Chin |
| 2011 | CSL | Non-Commutative Infinitary Peano Arithmetic. | Makoto Tatsuta, Stefano Berardi |
| 2011 | POPL | Static analysis of multi-staged programs via unstaging translation. | Wontae Choi, Baris Aktemur, Kwangkeun Yi, Makoto Tatsuta |
| 2010 | FLOPS | Internal Normalization, Compilation and Decompilation for System | Stefano Berardi, Makoto Tatsuta |
| 2009 | CSL | Non-Commutative First-Order Sequent Calculus. | Makoto Tatsuta |
| 2009 | SEFM | Completeness of Pointer Program Verification by Separation Logic. | Makoto Tatsuta, Wei-Ngan Chin, Mahmudul Faisal Al Ameen |
| 2008 | CSL | On Isomorphisms of Intersection Types. | Mariangiola Dezani-Ciancaglini, Roberto Di Cosmo, Elio Giovannetti, Makoto Tatsuta |
| 2008 | CSL | Undecidability of Type-Checking in Domain-Free Typed Lambda-Calculi with Existence. | Koji Nakazawa, Makoto Tatsuta, Yukiyoshi Kameyama, Hiroshi Nakano |
| 2008 | FLOPS | Types for Hereditary Head Normalizing Terms. | Makoto Tatsuta |
| 2008 | LICS | Types for Hereditary Permutators. | Makoto Tatsuta |
| 2007 | APLAS | Positive Arithmetic Without Exchange Is a Subclassical Logic. | Stefano Berardi, Makoto Tatsuta |
| 2006 | LICS | Normalisation is Insensible to lambda-Term Identity or Difference. | Makoto Tatsuta, Mariangiola Dezani-Ciancaglini |
| 1998 | LICS | Realizability for Constructive Theory of Functions and Classes and its Application to Program Synthesis. | Makoto Tatsuta |
| 1998 | MPC | Realizability of Monotone Coinductive Definitions and Its Application to Program Synthesis. | Makoto Tatsuta |