Takeshi Tsukada

According to our database, Takeshi Tsukada authored at least 56 papers between 2009 and 2025.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2025

Ranking and Invariants for Lower-Bound Inference in Quantitative Verification of Probabilistic Programs.

Satoshi Kura, Hiroshi Unno, Takeshi Tsukada

CoRR, April, 2025

A Primal-Dual Perspective on Program Verification Algorithms (Extended Version).

Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

CoRR, January, 2025

A Primal-Dual Perspective on Program Verification Algorithms.

Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham

Proc. ACM Program. Lang., 2025

Nola: Later-Free Ghost State for Verifying Termination in Iris.

Yusuke Matsushita, Takeshi Tsukada

Proc. ACM Program. Lang., 2025

Solving Higher-Order Quantified Boolean Satisfiability via Higher-Order Model Checking.

Hiroshi Unno, Takeshi Tsukada, Jie-Hong Roland Jiang

Proceedings of the AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 25, 2025

2024

Enriched Presheaf Model of Quantum FPC.

Takeshi Tsukada, Kazuyuki Asada

Proc. ACM Program. Lang., January, 2024

Inductive Approach to Spacer.

Takeshi Tsukada, Hiroshi Unno

Proc. ACM Program. Lang., 2024

Signature restriction for polymorphic algebraic effects.

Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi

J. Funct. Program., 2024

Hedge Automata Revisited: Transforming Texts to and from XML.

Akihisa Yamada, Jérémy Dubut, Takeshi Tsukada

Proceedings of the Automated Technology for Verification and Analysis, 2024

2023

HFL(Z) Validity Checking for Automated Program Verification.

Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada

Proc. ACM Program. Lang., January, 2023

Optimal CHC Solving via Termination Proofs.

Yu Gu, Takeshi Tsukada, Hiroshi Unno

Proc. ACM Program. Lang., January, 2023

2022

Software model-checking as cyclic-proof search.

Takeshi Tsukada, Hiroshi Unno

Proc. ACM Program. Lang., 2022

Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings.

Takeshi Tsukada, Kazuyuki Asada

CoRR, 2022

Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱.

Takeshi Tsukada, Kazuyuki Asada

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

2021

CPS transformation with affine types for call-by-value implicit polymorphism.

Taro Sekiyama, Takeshi Tsukada

Proc. ACM Program. Lang., 2021

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination.

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

CoRR, 2021

Enhancing Loop-Invariant Synthesis via Reinforcement Learning.

Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, Kohei Suenaga

CoRR, 2021

Counterexample generation for program verification based on ownership refinement types.

Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2021

Output Without Delay: A π-Calculus Compatible with Categorical Semantics.

Ken Sakayori, Takeshi Tsukada

Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

A Cyclic Proof System for HFL_ℕ.

Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination.

Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 2021

2020

A Cyclic Proof System for HFLN.

Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi

CoRR, 2020

RustHorn: CHC-based Verification for Rust Programs (full version).

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi

CoRR, 2020

Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking.

Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada

Proceedings of the Static Analysis - 27th International Symposium, 2020

On Computability of Logical Approaches to Branching-Time Property Verification of Programs.

Takeshi Tsukada

Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

On Average-Case Hardness of Higher-Order Model Checking.

Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

A Probabilistic Higher-Order Fixpoint Logic.

Yo Mitani, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

RustHorn: CHC-Based Verification for Rust Programs.

Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems, 2020

A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking.

Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 18th Asian Symposium, 2020

2019

Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence.

Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada

Log. Methods Comput. Sci., 2019

A Temporal Logic for Higher-Order Functional Programs.

Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Static Analysis - 26th International Symposium, 2019

Reduction from branching-time property verification of higher-order programs to HFL validity checking.

Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi

Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

A Categorical Model of an \mathbf i/o -typed \pi -calculus.

Ken Sakayori, Takeshi Tsukada

Proceedings of the Programming Languages and Systems, 2019

A Type-Based HFL Model Checking Algorithm.

Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

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

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Higher-Order Program Verification via HFL Model Checking.

Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe

Proceedings of the Programming Languages and Systems, 2018

Automated Synthesis of Functional Programs with Auxiliary Functions.

Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017

Streett Automata Model Checking of Higher-Order Recursion Schemes.

Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Verification of code generators via higher-order model checking.

Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi

Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2017

Generalised species of rigid resource terms.

Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong

Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence.

Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada

Proceedings of the Foundations of Software Science and Computation Structures, 2017

A Truly Concurrent Game Model of the Asynchronous \pi -Calculus.

Ken Sakayori, Takeshi Tsukada

Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016

Plays as Resource Terms via Non-idempotent Intersection Types.

Takeshi Tsukada, C.-H. Luke Ong

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Automatically disproving fair termination of higher-order functional programs.

Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation.

Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

Higher-Order Model Checking in Direct Style.

Taku Terao, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Nondeterminism in Game Semantics via Sheaves.

Takeshi Tsukada, C.-H. Luke Ong

Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014

Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence.

Takeshi Tsukada, C.-H. Luke Ong

CoRR, 2014

Complexity of Model-Checking Call-by-Value Programs.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Foundations of Software Science and Computation Structures, 2014

Unsafe Order-2 Tree Languages Are Context-Sensitive.

Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada

Proceedings of the Foundations of Software Science and Computation Structures, 2014

Compositional higher-order model checking via <i>ω</i>-regular games over Böhm trees.

Takeshi Tsukada, C.-H. Luke Ong

Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2012

An Intersection Type System for Deterministic Pushdown Automata.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Theoretical Computer Science, 2012

Two-Level Game Semantics, Intersection Types, and Recursion Schemes.

C.-H. Luke Ong, Takeshi Tsukada

Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

Exact Flow Analysis by Higher-Order Model Checking.

Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

2010

Untyped Recursion Schemes and Infinite Intersection Types.

Takeshi Tsukada, Naoki Kobayashi

Proceedings of the Foundations of Software Science and Computational Structures, 2010

2009

A Logical Foundation for Environment Classifiers.

Takeshi Tsukada, Atsushi Igarashi

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009