Takeshi Tsukada

Publication Activity (10 Years)

Years Active: 2009-2024
Publications (10 Years): 51

Top Topics

Top Venues

Proc. ACM Program. Lang.

Publications

Takeshi Tsukada, Hiroshi Unno
Inductive Approach to Spacer. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Takeshi Tsukada, Kazuyuki Asada
Enriched Presheaf Model of Quantum FPC. Proc. ACM Program. Lang. 8 (POPL) (2024)
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
Signature restriction for polymorphic algebraic effects. J. Funct. Program. 34 (2024)
Takeshi Tsukada, Kazuyuki Asada
Enriched Presheaf Model of Quantum FPC. CoRR (2023)
Yu Gu, Takeshi Tsukada, Hiroshi Unno
Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 7 (POPL) (2023)
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada
HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Takeshi Tsukada, Hiroshi Unno
Software model-checking as cyclic-proof search. Proc. ACM Program. Lang. 6 (POPL) (2022)
Takeshi Tsukada, Kazuyuki Asada
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings. CoRR (2022)
Takeshi Tsukada, Kazuyuki Asada
Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. LICS (2022)
Ken Sakayori, Takeshi Tsukada
Output Without Delay: A π-Calculus Compatible with Categorical Semantics. FSCD (2021)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-order Fixpoint Logic. Log. Methods Comput. Sci. 17 (4) (2021)
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. CoRR (2021)
Takeshi Tsukada, Hiroshi Unno
Software Model-Checking as Cyclic-Proof Search. CoRR (2021)
Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada
Counterexample generation for program verification based on ownership refinement types. PEPM@POPL (2021)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43 (4) (2021)
Taro Sekiyama, Takeshi Tsukada
CPS transformation with affine types for call-by-value implicit polymorphism. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, Kohei Suenaga
Enhancing Loop-Invariant Synthesis via Reinforcement Learning. CoRR (2021)
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A Cyclic Proof System for HFL_ℕ. CSL (2021)
Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada
Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. APLAS (2021)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-order Fixpoint Logic. CoRR (2020)
Yo Mitani, Naoki Kobayashi, Takeshi Tsukada
A Probabilistic Higher-Order Fixpoint Logic. FSCD (2020)
Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS (2020)
Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi
A Cyclic Proof System for HFLN. CoRR (2020)
Takeshi Tsukada
On Computability of Logical Approaches to Branching-Time Property Verification of Programs. LICS (2020)
Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS (2020)
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
Signature restriction for polymorphic algebraic effects. CoRR (2020)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-based Verification for Rust Programs (full version). CoRR (2020)
Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi
RustHorn: CHC-Based Verification for Rust Programs. ESOP (2020)
Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi
Signature restriction for polymorphic algebraic effects. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
On Average-Case Hardness of Higher-Order Model Checking. FSCD (2020)
Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi
Reduction from branching-time property verification of higher-order programs to HFL validity checking. PEPM@POPL (2019)
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Log. Methods Comput. Sci. 15 (1) (2019)
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
A Type-Based HFL Model Checking Algorithm. CoRR (2019)
Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada
A Type-Based HFL Model Checking Algorithm. APLAS (2019)
Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi
A Temporal Logic for Higher-Order Functional Programs. SAS (2019)
Ken Sakayori, Takeshi Tsukada
A Categorical Model of an \mathbf i/o -typed \pi -calculus. ESOP (2019)
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
Higher-Order Program Verification via HFL Model Checking. ESOP (2018)
Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada
Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS (2018)
Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. LICS (2018)
Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR (2018)
Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi
Verification of code generators via higher-order model checking. PEPM (2017)
Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS (2017)
Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
Generalised species of rigid resource terms. LICS (2017)
Ken Sakayori, Takeshi Tsukada
A Truly Concurrent Game Model of the Asynchronous \pi -Calculus. FoSSaCS (2017)
Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada
Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD (2017)
Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe
Higher-Order Program Verification via HFL Model Checking. CoRR (2017)
Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi
Automatically disproving fair termination of higher-order functional programs. ICFP (2016)
Taku Terao, Takeshi Tsukada, Naoki Kobayashi
Higher-Order Model Checking in Direct Style. APLAS (2016)
Takeshi Tsukada, C.-H. Luke Ong
Plays as Resource Terms via Non-idempotent Intersection Types. LICS (2016)
Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. APLAS (2016)
Takeshi Tsukada, C.-H. Luke Ong
Nondeterminism in Game Semantics via Sheaves. LICS (2015)
Takeshi Tsukada, C.-H. Luke Ong
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR (2014)
Takeshi Tsukada, Naoki Kobayashi
Complexity of Model-Checking Call-by-Value Programs. FoSSaCS (2014)
Takeshi Tsukada, C.-H. Luke Ong
-regular games over Böhm trees. CSL-LICS (2014)
Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada
Unsafe Order-2 Tree Languages Are Context-Sensitive. FoSSaCS (2014)
Takeshi Tsukada, Naoki Kobayashi
An Intersection Type System for Deterministic Pushdown Automata. IFIP TCS (2012)
C.-H. Luke Ong, Takeshi Tsukada
Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP (2) (2012)
Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi
Exact Flow Analysis by Higher-Order Model Checking. FLOPS (2012)
Takeshi Tsukada, Naoki Kobayashi
Untyped Recursion Schemes and Infinite Intersection Types. FoSSaCS (2010)
Takeshi Tsukada, Atsushi Igarashi
A Logical Foundation for Environment Classifiers Log. Methods Comput. Sci. 6 (4) (2010)
Takeshi Tsukada, Atsushi Igarashi
A Logical Foundation for Environment Classifiers. TLCA (2009)