Untyped Recursion Schemes and Infinite Intersection Types. - Takeshi Tsukada; Naoki Kobayashi 001 (FoSSaCS, 2010)

A Logical Foundation for Environment Classifiers - Takeshi Tsukada; Atsushi Igarashi (Log. Methods Comput. Sci., 2010)

Exact Flow Analysis by Higher-Order Model Checking. - Yoshihiro Tobita; Takeshi Tsukada; Naoki Kobayashi 001 (FLOPS, 2012)

Two-Level Game Semantics, Intersection Types, and Recursion Schemes. - C.-H. Luke Ong; Takeshi Tsukada (ICALP (2), 2012)

An Intersection Type System for Deterministic Pushdown Automata. - Takeshi Tsukada; Naoki Kobayashi 001 (IFIP TCS, 2012)

Compositional higher-order model checking via ω-regular games over Böhm trees. - Takeshi Tsukada; C.-H. Luke Ong (CSL-LICS, 2014)

Unsafe Order-2 Tree Languages Are Context-Sensitive. - Naoki Kobayashi 001; Kazuhiro Inaba; Takeshi Tsukada (FoSSaCS, 2014)

Complexity of Model-Checking Call-by-Value Programs. - Takeshi Tsukada; Naoki Kobayashi 001 (FoSSaCS, 2014)

Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. - Takeshi Tsukada; C.-H. Luke Ong (CoRR, 2014)

Nondeterminism in Game Semantics via Sheaves. - Takeshi Tsukada; C.-H. Luke Ong (LICS, 2015)

Higher-Order Model Checking in Direct Style. - Taku Terao; Takeshi Tsukada; Naoki Kobayashi 001 (APLAS, 2016)

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. - Kazuhide Yasukata; Takeshi Tsukada; Naoki Kobayashi 001 (APLAS, 2016)

Automatically disproving fair termination of higher-order functional programs. - Keiichi Watanabe; Ryosuke Sato 001; Takeshi Tsukada; Naoki Kobayashi 001 (ICFP, 2016)

Plays as Resource Terms via Non-idempotent Intersection Types. - Takeshi Tsukada; C.-H. Luke Ong (LICS, 2016)

A Truly Concurrent Game Model of the Asynchronous pi -Calculus. - Ken Sakayori; Takeshi Tsukada (FoSSaCS, 2017)

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. - Ryoma Sin'ya; Kazuyuki Asada; Naoki Kobayashi 001; Takeshi Tsukada (FoSSaCS, 2017)

Generalised species of rigid resource terms. - Takeshi Tsukada; Kazuyuki Asada; C.-H. Luke Ong (LICS, 2017)

Verification of code generators via higher-order model checking. - Takashi Suwa; Takeshi Tsukada; Naoki Kobayashi 001; Atsushi Igarashi (PEPM, 2017)

Streett Automata Model Checking of Higher-Order Recursion Schemes. - Ryota Suzuki 002; Koichi Fujima; Naoki Kobayashi 001; Takeshi Tsukada (FSCD, 2017)

Automated Synthesis of Functional Programs with Auxiliary Functions. - Shingo Eguchi; Naoki Kobayashi 001; Takeshi Tsukada (APLAS, 2018)

Higher-Order Program Verification via HFL Model Checking. - Naoki Kobayashi 001; Takeshi Tsukada; Keiichi Watanabe (ESOP, 2018)

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 (LICS, 2018)

A Type-Based HFL Model Checking Algorithm. - Youkichi Hosoi; Naoki Kobayashi 001; Takeshi Tsukada (APLAS, 2019)

A Categorical Model of an mathbf i/o -typed pi -calculus. - Ken Sakayori; Takeshi Tsukada (ESOP, 2019)

Reduction from branching-time property verification of higher-order programs to HFL validity checking. - Keiichi Watanabe; Takeshi Tsukada; Hiroki Oshikawa; Naoki Kobayashi 001 (PEPM@POPL, 2019)

A Temporal Logic for Higher-Order Functional Programs. - Yuya Okuyama; Takeshi Tsukada; Naoki Kobayashi 001 (SAS, 2019)

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. - Kazuyuki Asada; Naoki Kobayashi 001; Ryoma Sin'ya; Takeshi Tsukada (Log. Methods Comput. Sci., 2019)

A New Refinement Type System for Automated $ nu text {HFL}_ mathbb {Z}$ Validity Checking. - Hiroyuki Katsura; Naoki Iwayama; Naoki Kobayashi 001; Takeshi Tsukada (APLAS, 2020)

On Average-Case Hardness of Higher-Order Model Checking. - Yoshiki Nakamura 001; Kazuyuki Asada; Naoki Kobayashi 001; Ryoma Sin'ya; Takeshi Tsukada (FSCD, 2020)

On Computability of Logical Approaches to Branching-Time Property Verification of Programs. - Takeshi Tsukada (LICS, 2020)

Predicate Abstraction and CEGAR for $ nu mathrm {HFL}_ mathbb {Z}$ Validity Checking. - Naoki Iwayama; Naoki Kobayashi 001; Ryota Suzuki 002; Takeshi Tsukada (SAS, 2020)

RustHorn: CHC-based Verification for Rust Programs (full version). - Yusuke Matsushita 002; Takeshi Tsukada; Naoki Kobayashi 001 (CoRR, 2020)

A Cyclic Proof System for HFLN. - Mayuko Kori; Takeshi Tsukada; Naoki Kobayashi 001 (CoRR, 2020)

Signature restriction for polymorphic algebraic effects. - Taro Sekiyama; Takeshi Tsukada; Atsushi Igarashi (Proc. ACM Program. Lang., 2020)

Termination Analysis for the $$ pi $$-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (APLAS, 2021)

A Cyclic Proof System for HFL_ℕ. - Mayuko Kori; Takeshi Tsukada; Naoki Kobayashi 001 (CSL, 2021)

Output Without Delay: A π-Calculus Compatible with Categorical Semantics. - Ken Sakayori; Takeshi Tsukada (FSCD, 2021)

Counterexample generation for program verification based on ownership refinement types. - Hideto Ueno; John Toman; Naoki Kobayashi 001; Takeshi Tsukada (PEPM@POPL, 2021)

Enhancing Loop-Invariant Synthesis via Reinforcement Learning. - Takeshi Tsukada; Hiroshi Unno 001; Taro Sekiyama; Kohei Suenaga (CoRR, 2021)

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. - Tsubasa Shoshi; Takuma Ishikawa; Naoki Kobayashi 001; Ken Sakayori; Ryosuke Sato 001; Takeshi Tsukada (CoRR, 2021)

A Probabilistic Higher-order Fixpoint Logic. - Yo Mitani; Naoki Kobayashi 001; Takeshi Tsukada (Log. Methods Comput. Sci., 2021)

CPS transformation with affine types for call-by-value implicit polymorphism. - Taro Sekiyama; Takeshi Tsukada (Proc. ACM Program. Lang., 2021)

RustHorn: CHC-based Verification for Rust Programs. - Yusuke Matsushita 002; Takeshi Tsukada; Naoki Kobayashi 001 (ACM Trans. Program. Lang. Syst., 2021)

Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. - Takeshi Tsukada; Kazuyuki Asada (LICS, 2022)

Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings. - Takeshi Tsukada; Kazuyuki Asada (CoRR, 2022)

Software model-checking as cyclic-proof search. - Takeshi Tsukada; Hiroshi Unno 001 (Proc. ACM Program. Lang., 2022)

Optimal CHC Solving via Termination Proofs. - Yu Gu 022; Takeshi Tsukada; Hiroshi Unno 001 (Proc. ACM Program. Lang., 2023)

HFL(Z) Validity Checking for Automated Program Verification. - Naoki Kobayashi 001; Kento Tanahashi; Ryosuke Sato 001; Takeshi Tsukada (Proc. ACM Program. Lang., 2023)

Hedge Automata Revisited: Transforming Texts to and from XML. - Akihisa Yamada 002; Jérémy Dubut; Takeshi Tsukada (ATVA (2), 2024)

Inductive Approach to Spacer. - Takeshi Tsukada; Hiroshi Unno 001 (Proc. ACM Program. Lang., 2024)

Enriched Presheaf Model of Quantum FPC. - Takeshi Tsukada; Kazuyuki Asada (Proc. ACM Program. Lang., 2024)

Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking. - Hiroshi Unno 001; Takeshi Tsukada; Jie-Hong Roland Jiang (AAAI, 2025)

Nola: Later-Free Ghost State for Verifying Termination in Iris. - Yusuke Matsushita 002; Takeshi Tsukada (Proc. ACM Program. Lang., 2025)

A Primal-Dual Perspective on Program Verification Algorithms. - Takeshi Tsukada; Hiroshi Unno 001; Oded Padon; Sharon Shoham (Proc. ACM Program. Lang., 2025)

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version). - Takeshi Tsukada; Hiroshi Unno 001; Oded Padon; Sharon Shoham (CoRR, 2025)

Ranking and Invariants for Lower-Bound Inference in Quantitative Verification of Probabilistic Programs. - Satoshi Kura 001; Hiroshi Unno 001; Takeshi Tsukada (CoRR, 2025)