Takeshi Tsukada

67 papers A* 7A 4B 18C 1Misc 1Journal 29Unranked 7

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