| 2021 | APLAS | Function Pointer Eliminator for C Programs. | Daisuke Kimura, Mahmudul Faisal Al Ameen, Makoto Tatsuta, Koji Nakazawa |
| 2021 | FSCD | Failure of Cut-Elimination in the Cyclic Proof System of Bunched Logic with Inductive Propositions. | Kenji Saotome, Koji Nakazawa, Daisuke Kimura |
| 2020 | FLOPS | Restriction on Cut in Cyclic Proof System for Symbolic Heaps. | Kenji Saotome, Koji Nakazawa, Daisuke Kimura |
| 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 |
| 2015 | APLAS | Separation Logic with Monadic Inductive Definitions and Implicit Existentials. | Makoto Tatsuta, Daisuke Kimura |
| 2012 | ICML | Fast Computation of Subpath Kernel for Trees. | Daisuke Kimura, Hisashi Kashima |
| 2011 | PAKDD | A Subpath Kernel for Rooted Unordered Trees. | Daisuke Kimura, Tetsuji Kuboyama, Tetsuo Shibuya, Hisashi Kashima |
| 2009 | APLAS | Classical Natural Deduction for S4 Modal Logic. | Daisuke Kimura, Yoshihiko Kakutani |
| 2007 | APLAS | Call-by-Value Is Dual to Call-by-Name, Extended. | Daisuke Kimura |