A Primal-Dual Perspective on Program Verification Algorithms Takeshi Tsukada, Hiroshi Unno, Oded Padon, Sharon Shoham Proc. ACM Program. Lang. (PLDI), 2024, accepted
Signature restriction for polymorphic algebraic effects Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi Journal of Functional Programming, vol.32, e7, 2024 DOI
Inductive Approach to Spacer Takeshi Tsukada, Hiroshi Unno Proc. ACM Program. Lang. (PLDI), vol. 8, pp.1979--2002, 2024 DOI
Enriched Presheaf Model of Quantum FPC Takeshi Tsukada, Kazuyuki Asada Proc. ACM Program. Lang. (POPL), vol. 8, pp.362--392, 2024 arXiv|
DOI
HFL(Z) Validity Checking for Automated Program Verification Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada Proc. ACM Program. Lang. (POPL), vol. 7, pp.154--184, 2023 DOI
Optimal CHC Solving via Termination Proofs Yu Gu, Takeshi Tsukada, Hiroshi Unno Proc. ACM Program. Lang. (POPL), vol. 7, pp.604--631, 2023 DOI
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings Takeshi Tsukada, Kazuyuki Asada In Proc. of: the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022), pp.60:1--60:13, ACM, 2022 arXiv |
DOI
Software model-checking as cyclic-proof search Takeshi Tsukada, Hiroshi Unno Proc. ACM Program. Lang. (POPL), vol. 6, pp.1--29, 2022 arXiv |
DOI
Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada In Proc. of: the 19th Asian Symposium on Programming Languages and Systems (APLAS 2021), LNCS 13008, pp.265--284, Springer, 2021 DOI
CPS transformation with affine types for call-by-value implicit polymorphism Taro Sekiyama, Takeshi Tsukada Proc. ACM Program. Lang. (ICFP), vol. 5, pp.1—30, 2021 DOI
A Cyclic Proof System for HFLN Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), LIPIcs 183, pp.29:1--29:22, Schloss Dagstuhl, 2021 arXiv |
DOI
Output Without Delay: A π-Calculus Compatible with Categorical Semantics Ken Sakayori, Takeshi Tsukada In Proc. of: the 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), LIPIcs 195, pp.32:1--32:22, Schloss Dagstuhl, 2021 DOI
Counterexample generation for program verification based on ownership refinement types Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada In Proc. of: the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM@POPL 2021), pp.44--57, ACM, 2021 DOI
A New Refinement Type System for Automated νHFLZ Validity Checking Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada In Proc. of: the 18th Asian Symposium on Programming Languages and Systems (APLAS 2020), LNCS 12470, pp. 86--104, Springer, 2020 DOI
Signature restriction for polymorphic algebraic effects Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi Proc. ACM Program. Lang. (ICFP), vol.4, pp.117:1--117:30, 2020 arXiv |
DOI
Probabilistic Higher-Order Fixpoint Logic Yo Mitani, Naoki Kobayashi, Takeshi Tsukada In Proc. of: the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp. 19:1--19:22, Schloss Dagstuhl, 2020 PDF |
DOI |
journal version
On Average-Case Hardness of Higher-Order Model Checking Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya and Takeshi Tsukada In Proc. of: the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), LIPIcs 167, pp.21:1--21:23, Schloss Dagstuhl, 2020 PDF |
DOI
On Computability of Logical Approaches to Branching-Time Property Verification of Programs Takeshi Tsukada In Proc of: the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2020), pp.886—899, ACM, 2020 DOI
Predicate Abstraction and CEGAR for νHFLZ Validity Checking Naoki Iwayama, Naoki Kobayashi, Ryota Suzuki, Takeshi Tsukada In Proc. of: the 27th Static Analysis Symposium (SAS 2020), LNCS 12389, pp.134--155, Springer, 2020 DOI
A Type-Based HFL Model Checking Algorithm Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada In Proc. of: the 17th Asian Symposium on Programming Languages and Systems (APLAS 2019), LNCS 11893, pp.136--155, Springer, 2019 PDF |
DOI
A Temporal Logic for Higher-Order Functional Programs Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 26th Static Analysis Symposium (SAS 2019), LNCS 11822, pp.437-458, Springer, 2019 DOI
A Categorical Model of an i/o-typed pi-calculus Ken Sakayori, Takeshi Tsukada In Proc. of: the 28th European Symposium on Programming (ESOP 2019), LNCS 11423, pp.640-667, Springer, 2019 DOI
Reduction from branching-time property verification of higher-order programs to HFL validity checking Keiichi Watanabe, Takeshi Tsukada, Hiroki Oshikawa, Naoki Kobayashi In Proc. of: the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM@POPL 2019), pp.22-34, ACM, 2019 DOI
Automated Synthesis of Functional Programs with Auxiliary Functions Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada In Proc. of: 16th Asian Symposium on Programming Languages and Systems (APLAS 2018), LNCS 11275, pp.223-241, Springer, 2018 DOI
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 In Prof. of: the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018), pp.889-898, ACM, 2018 author version (in preparation) |
DOI
Higher-Order Program Verification via HFL Model Checking Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe In Proc. of: the 27th European Symposium on Programming (ESOP 2018), LNCS 10801, pp. 711-738, Springer, 2018 arXiv |
DOI
A Truly Concurrent Game Model of the Asynchronous pi-Calculus Ken Sakayori, Takeshi Tsukada In Proc. of: the 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), LNCS 10203, pp.389-406, Springer, 2017 DOI
Generalised species of rigid resource terms Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong In Proc. of: the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017), pp.1-12, IEEE Computer Society, 2017 long version (in preparation) |
DOI
Streett Automata Model Checking of Higher-Order Recursion Schemes Ryota Suzuki, Koichi Fujima, Naoki Kobayashi, Takeshi Tsukada In Proc. of: the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017). LIPIcs 84, pp. 32:1-32:18, Schloss Dagstuhl, 2017 PDF |
DOI
Verification of code generators via higher-order model checking Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi In Proc. of: the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM@POPL 2017), ACM, pp.59-70, 2017 DOI
Automatically disproving fair termination of higher-order functional programs Keiichi Watanabe, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.243-255, ACM, 2016 DOI
Higher-Order Model Checking in Direct Style Taku Terao, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 14th Asian Symposium on Programming Languages and Systems (APLAS 2016), LNCS 10017, pp.295-313, Springer, 2016 DOI
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 14th Asian Symposium on Programming Languages and Systems (APLAS 2016), LNCS 10017, pp.335-353, Springer, 2016 DOI
Plays as Resource Terms via Non-idempotent Intersection Types Takeshi Tsukada, C.-H. Luke Ong In Proc. of: the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), pp.237-246, ACM, 2016 long version (in preparation) |
DOI
Nondeterminism in Game Semantics via Sheaves Takeshi Tsukada, C.-H. Luke Ong In Proc. of: the 30th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2015), pp.220-231, IEEE Computer Society , 2015 long version (in preparation) |
DOI |
a preliminary version (arXiv)
Compositional higher-order model checking via ω-regular games over Böhm trees Takeshi Tsukada, C.-H. Luke Ong In Proc. of: Joint Meeting of the 33rd EACSL Annual Conference on Computer Science Logic and the 29th Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS 2014), pp78:1-78:10, ACM, 2014 long version (in preparation) |
DOI
Unsafe Order-2 Tree Languages Are Context-Sensitive Naoki Kobayashi, Kazuhiro Inaba, Takeshi Tsukada In Proc. of: the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2014), LNCS 8412, pp.149-163, Springer, 2014 Best EATPS Paper Aword (EATCS) PDF |
DOI
Complexity of Model-Checking Call-by-Value Programs Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 17th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2014), LNCS 8412, pp.180-194, Springer, 2014 DOI
Exact Flow Analysis by Higher-Order Model Checking Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 11th International Symposium on Functional and Logic Programming (FLOPS 2012), LNCS 7292, pp.275-289, Springer, 2012 DOI
Two-Level Game Semantics, Intersection Types, and Recursion Schemes C.-H. Luke Ong, Takeshi Tsukada In Proc. of: the 39th International Colloquium on Automata, Languages, and Programming (ICALP Track B 2012), LNCS 7392, pp.325-336, Springer, 2012 DOI
An Intersection Type System for Deterministic Pushdown Automata Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 7th IFIP TC 1/WG 2.2 International Conference on Theoretical Computer Science (IFIP-TCS 2012), LNCS 7604, pp.357-371, Springer, 2012 hal |
DOI
文脈自由言語と超決定性言語の包含判定問題の決定可能性の型理論を用いた証明 塚田武志, 小林直樹 情報処理学会論文誌プログラミング (PRO), 4(2), pp.31-47, 情報処理学会, 2011 PDF
Untyped Recursion Schemes and Infinite Intersection Types Takeshi Tsukada, Naoki Kobayashi In Proc. of: the 13th International Conference on Foundations of Software Science and Computational Structures (FoSSaCS 2010), LNCS 6014, pp.343-357, Springer, 2010 PDF |
DOI