default search action
Takeshi Tsukada
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Journal Articles
- 2024
- [j12]Taro Sekiyama
, Takeshi Tsukada
Signature restriction for polymorphic algebraic effects. J. Funct. Program. 34 (2024) - [j11]Takeshi Tsukada
Inductive Approach to Spacer. Proc. ACM Program. Lang. 8(PLDI): 1979-2002 (2024) - [j10]Takeshi Tsukada
Enriched Presheaf Model of Quantum FPC. Proc. ACM Program. Lang. 8(POPL): 362-392 (2024) - 2023
- [j9]Naoki Kobayashi
HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 7(POPL): 154-184 (2023) - [j8]Yu Gu
Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 7(POPL): 604-631 (2023) - 2022
- [j7]Takeshi Tsukada
Software model-checking as cyclic-proof search. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) - 2021
- [j6]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-order Fixpoint Logic. Log. Methods Comput. Sci. 17(4) (2021) - [j5]Taro Sekiyama
CPS transformation with affine types for call-by-value implicit polymorphism. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j4]Yusuke Matsushita
RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4): 15:1-15:54 (2021) - 2020
- [j3]Taro Sekiyama
Signature restriction for polymorphic algebraic effects. Proc. ACM Program. Lang. 4(ICFP): 117:1-117:30 (2020) - 2019
- [j2]Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. Log. Methods Comput. Sci. 15(1) (2019) - 2010
- [j1]Takeshi Tsukada, Atsushi Igarashi
A Logical Foundation for Environment Classifiers. Log. Methods Comput. Sci. 6(4) (2010)
Conference and Workshop Papers
- 2022
- [c36]Takeshi Tsukada, Kazuyuki Asada:
Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. LICS 2022: 60:1-60:13 - 2021
- [c35]Tsubasa Shoshi
Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination. APLAS 2021: 265-284 - [c34]Mayuko Kori
A Cyclic Proof System for HFL_ℕ. CSL 2021: 29:1-29:22 - [c33]Ken Sakayori
Output Without Delay: A π-Calculus Compatible with Categorical Semantics. FSCD 2021: 32:1-32:22 - [c32]Hideto Ueno, John Toman, Naoki Kobayashi
Counterexample generation for program verification based on ownership refinement types. PEPM@POPL 2021: 44-57 - 2020
- [c31]Hiroyuki Katsura
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS 2020: 86-104 - [c30]Yusuke Matsushita
RustHorn: CHC-Based Verification for Rust Programs. ESOP 2020: 484-514 - [c29]Yo Mitani, Naoki Kobayashi
A Probabilistic Higher-Order Fixpoint Logic. FSCD 2020: 19:1-19:22 - [c28]Yoshiki Nakamura
On Average-Case Hardness of Higher-Order Model Checking. FSCD 2020: 21:1-21:23 - [c27]Takeshi Tsukada:
On Computability of Logical Approaches to Branching-Time Property Verification of Programs. LICS 2020: 886-899 - [c26]Naoki Iwayama, Naoki Kobayashi
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS 2020: 134-155 - 2019
- [c25]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. APLAS 2019: 136-155 - [c24]Ken Sakayori
A Categorical Model of an \mathbf i/o -typed \pi -calculus. ESOP 2019: 640-667 - [c23]Keiichi Watanabe
Reduction from branching-time property verification of higher-order programs to HFL validity checking. PEPM@POPL 2019: 22-34 - [c22]Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi:
A Temporal Logic for Higher-Order Functional Programs. SAS 2019: 437-458 - 2018
- [c21]Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada:
Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS 2018: 223-241 - [c20]Naoki Kobayashi
Higher-Order Program Verification via HFL Model Checking. ESOP 2018: 711-738 - [c19]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: 889-898 - 2017
- [c18]Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS 2017: 53-68 - [c17]Ken Sakayori
A Truly Concurrent Game Model of the Asynchronous \pi -Calculus. FoSSaCS 2017: 389-406 - [c16]Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong:
Generalised species of rigid resource terms. LICS 2017: 1-12 - [c15]Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi, Atsushi Igarashi
Verification of code generators via higher-order model checking. PEPM 2017: 59-70 - [c14]Ryota Suzuki, Koichi Fujima, Naoki Kobayashi
Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD 2017: 32:1-32:18 - 2016
- [c13]Taku Terao, Takeshi Tsukada, Naoki Kobayashi
Higher-Order Model Checking in Direct Style. APLAS 2016: 295-313 - [c12]Kazuhide Yasukata, Takeshi Tsukada, Naoki Kobayashi
Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation. APLAS 2016: 335-353 - [c11]Keiichi Watanabe
Automatically disproving fair termination of higher-order functional programs. ICFP 2016: 243-255 - [c10]Takeshi Tsukada, C.-H. Luke Ong:
Plays as Resource Terms via Non-idempotent Intersection Types. LICS 2016: 237-246 - 2015
- [c9]Takeshi Tsukada, C.-H. Luke Ong
Nondeterminism in Game Semantics via Sheaves. LICS 2015: 220-231 - 2014
- [c8]Takeshi Tsukada, C.-H. Luke Ong
Compositional higher-order model checking via ω-regular games over Böhm trees. CSL-LICS 2014: 78:1-78:10 - [c7]Naoki Kobayashi
Unsafe Order-2 Tree Languages Are Context-Sensitive. FoSSaCS 2014: 149-163 - [c6]Takeshi Tsukada, Naoki Kobayashi
Complexity of Model-Checking Call-by-Value Programs. FoSSaCS 2014: 180-194 - 2012
- [c5]Yoshihiro Tobita, Takeshi Tsukada, Naoki Kobayashi
Exact Flow Analysis by Higher-Order Model Checking. FLOPS 2012: 275-289 - [c4]C.-H. Luke Ong
Two-Level Game Semantics, Intersection Types, and Recursion Schemes. ICALP (2) 2012: 325-336 - [c3]Takeshi Tsukada, Naoki Kobayashi
An Intersection Type System for Deterministic Pushdown Automata. IFIP TCS 2012: 357-371 - 2010
- [c2]Takeshi Tsukada, Naoki Kobayashi
Untyped Recursion Schemes and Infinite Intersection Types. FoSSaCS 2010: 343-357 - 2009
- [c1]Takeshi Tsukada, Atsushi Igarashi:
A Logical Foundation for Environment Classifiers. TLCA 2009: 341-355
Informal and Other Publications
- 2023
- [i13]Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. CoRR abs/2311.03117 (2023) - 2022
- [i12]Takeshi Tsukada, Kazuyuki Asada:
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings. CoRR abs/2204.10589 (2022) - 2021
- [i11]Takeshi Tsukada, Hiroshi Unno, Taro Sekiyama, Kohei Suenaga:
Enhancing Loop-Invariant Synthesis via Reinforcement Learning. CoRR abs/2107.09766 (2021) - [i10]Tsubasa Shoshi, Takuma Ishikawa, Naoki Kobayashi, Ken Sakayori, Ryosuke Sato, Takeshi Tsukada:
Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination. CoRR abs/2109.00311 (2021) - [i9]Takeshi Tsukada, Hiroshi Unno:
Software Model-Checking as Cyclic-Proof Search. CoRR abs/2111.05617 (2021) - 2020
- [i8]Yusuke Matsushita
RustHorn: CHC-based Verification for Rust Programs (full version). CoRR abs/2002.09002 (2020) - [i7]Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi:
Signature restriction for polymorphic algebraic effects. CoRR abs/2003.08138 (2020) - [i6]Mayuko Kori
A Cyclic Proof System for HFLN. CoRR abs/2010.14891 (2020) - [i5]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-order Fixpoint Logic. CoRR abs/2011.14303 (2020) - 2019
- [i4]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. CoRR abs/1908.10416 (2019) - 2018
- [i3]Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR abs/1801.03886 (2018) - 2017
- [i2]Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
Higher-Order Program Verification via HFL Model Checking. CoRR abs/1710.08614 (2017) - 2014
- [i1]Takeshi Tsukada, C.-H. Luke Ong:
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR abs/1409.2764 (2014)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 21:16 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: