| 2026 | CAV | Lagrangian-Based Duality for Quantified SMT Algorithms. | Ivana Bocevska, Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham |
| 2026 | FSCD | Stabilized Profunctors and Matrix Representation. | Takeshi Tsukada, Kazuyuki Asada, Kengo Hirata |
| 2026 | LICS | Causality in Pure Quantum Computation with Quantum Control. | Kengo Hirata, Takeshi Tsukada |
| 2025 | AAAI | Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking. | Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang |
| 2024 | ATVA | Hedge Automata Revisited: Transforming Texts to and from XML. | Akihisa Yamada, Jrmy Dubut, Takeshi Tsukada |
| 2022 | LICS | Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. | Takeshi Tsukada, Kazuyuki Asada |
| 2021 | APLAS | Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. | Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada |
| 2021 | CSL | A Cyclic Proof System for HFL_ℕ. | Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi |
| 2021 | FSCD | Output Without Delay: A π-Calculus Compatible with Categorical Semantics. | Ken Sakayori, Takeshi Tsukada |
| 2021 | PEPM | Counterexample generation for program verification based on ownership refinement types. | Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada |
| 2020 | APLAS | A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. | Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada |
| 2020 | ESOP | RustHorn: CHC-Based Verification for Rust Programs. | Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi |
| 2020 | FSCD | A Probabilistic Higher-Order Fixpoint Logic. | Yo Mitani, Naoki Kobayashi, Takeshi Tsukada |
| 2020 | FSCD | On Average-Case Hardness of Higher-Order Model Checking. | Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada |
| 2020 | LICS | On Computability of Logical Approaches to Branching-Time Property Verification of Programs. | Takeshi Tsukada |
| 2020 | SAS | Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. | Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada |
| 2019 | APLAS | A Type-Based HFL Model Checking Algorithm. | Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada |
| 2019 | ESOP | A Categorical Model of an \mathbf i/o -typed \pi -calculus. | Ken Sakayori, Takeshi Tsukada |
| 2019 | PEPM | Reduction from branching-time property verification of higher-order programs to HFL validity checking. | Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi |
| 2019 | SAS | A Temporal Logic for Higher-Order Functional Programs. | Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi |
| 2018 | APLAS | Automated Synthesis of Functional Programs with Auxiliary Functions. | Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada |
| 2018 | ESOP | Higher-Order Program Verification via HFL Model Checking. | Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe |
| 2018 | LICS | Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. | Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong |
| 2017 | FOSSACS | A Truly Concurrent Game Model of the Asynchronous \pi -Calculus. | Ken Sakayori, Takeshi Tsukada |
| 2017 | FOSSACS | Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. | Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada |
| 2017 | LICS | Generalised species of rigid resource terms. | Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong |
| 2017 | PEPM | Verification of code generators via higher-order model checking. | Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi |
| 2016 | APLAS | Higher-Order Model Checking in Direct Style. | Taku Terao, Takeshi Tsukada, Naoki Kobayashi |
| 2016 | APLAS | Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. | Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi |
| 2016 | ICFP | Automatically disproving fair termination of higher-order functional programs. | Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi |
| 2016 | LICS | Plays as Resource Terms via Non-idempotent Intersection Types. | Takeshi Tsukada, C.-H. Luke Ong |
| 2015 | LICS | Nondeterminism in Game Semantics via Sheaves. | Takeshi Tsukada, C.-H. Luke Ong |
| 2014 | CSL | Compositional higher-order model checking via | Takeshi Tsukada, C.-H. Luke Ong |
| 2014 | FOSSACS | Unsafe Order-2 Tree Languages Are Context-Sensitive. | Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada |
| 2014 | FOSSACS | Complexity of Model-Checking Call-by-Value Programs. | Takeshi Tsukada, Naoki Kobayashi |
| 2012 | FLOPS | Exact Flow Analysis by Higher-Order Model Checking. | Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi |
| 2012 | ICALP | Two-Level Game Semantics, Intersection Types, and Recursion Schemes. | C.-H. Luke Ong, Takeshi Tsukada |
| 2010 | FOSSACS | Untyped Recursion Schemes and Infinite Intersection Types. | Takeshi Tsukada, Naoki Kobayashi |