default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDTakeshi Tsukada
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j12]Taro Sekiyama
, Takeshi Tsukada, Atsushi Igarashi:
Signature restriction for polymorphic algebraic effects. J. Funct. Program. 34 (2024)- [j11]Takeshi Tsukada, Hiroshi Unno:
Inductive Approach to Spacer. Proc. ACM Program. Lang. 8(PLDI): 1979-2002 (2024) - [j10]Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. Proc. ACM Program. Lang. 8(POPL): 362-392 (2024) - 2023
- [j9]Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada:
HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 7(POPL): 154-184 (2023) - [j8]Yu Gu, Takeshi Tsukada, Hiroshi Unno:
Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 7(POPL): 604-631 (2023) - [i13]Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. CoRR abs/2311.03117 (2023) - 2022
- [j7]Takeshi Tsukada, Hiroshi Unno:
Software model-checking as cyclic-proof search. Proc. ACM Program. Lang. 6(POPL): 1-29 (2022) - [c36]Takeshi Tsukada, Kazuyuki Asada:
Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱. LICS 2022: 60:1-60:13 - [i12]Takeshi Tsukada, Kazuyuki Asada:
Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings. CoRR abs/2204.10589 (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, Takeshi Tsukada:
CPS transformation with affine types for call-by-value implicit polymorphism. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j4]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
RustHorn: CHC-based Verification for Rust Programs. ACM Trans. Program. Lang. Syst. 43(4): 15:1-15:54 (2021) - [c35]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: 265-284 - [c34]Mayuko Kori, Takeshi Tsukada, Naoki Kobayashi:
A Cyclic Proof System for HFL_ℕ. CSL 2021: 29:1-29:22 - [c33]Ken Sakayori, Takeshi Tsukada:
Output Without Delay: A π-Calculus Compatible with Categorical Semantics. FSCD 2021: 32:1-32:22 - [c32]Hideto Ueno, John Toman, Naoki Kobayashi, Takeshi Tsukada:
Counterexample generation for program verification based on ownership refinement types. PEPM@POPL 2021: 44-57 - [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
- [j3]Taro Sekiyama, Takeshi Tsukada, Atsushi Igarashi:
Signature restriction for polymorphic algebraic effects. Proc. ACM Program. Lang. 4(ICFP): 117:1-117:30 (2020) - [c31]Hiroyuki Katsura, Naoki Iwayama, Naoki Kobayashi, Takeshi Tsukada:
A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking. APLAS 2020: 86-104 - [c30]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
RustHorn: CHC-Based Verification for Rust Programs. ESOP 2020: 484-514 - [c29]Yo Mitani, Naoki Kobayashi, Takeshi Tsukada:
A Probabilistic Higher-Order Fixpoint Logic. FSCD 2020: 19:1-19:22 - [c28]Yoshiki Nakamura, Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada:
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, Ryota Suzuki, Takeshi Tsukada:
Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking. SAS 2020: 134-155 - [i8]Yusuke Matsushita, Takeshi Tsukada, Naoki Kobayashi:
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, Takeshi Tsukada, Naoki Kobayashi:
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)
2010 – 2019
- 2019
- [j2]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) - [c25]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. APLAS 2019: 136-155 - [c24]Ken Sakayori, Takeshi Tsukada:
A Categorical Model of an \mathbf i/o -typed \pi -calculus. ESOP 2019: 640-667 - [c23]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: 22-34 - [c22]Yuya Okuyama, Takeshi Tsukada, Naoki Kobayashi:
A Temporal Logic for Higher-Order Functional Programs. SAS 2019: 437-458 - [i4]Youkichi Hosoi, Naoki Kobayashi, Takeshi Tsukada:
A Type-Based HFL Model Checking Algorithm. CoRR abs/1908.10416 (2019) - 2018
- [c21]Shingo Eguchi, Naoki Kobayashi, Takeshi Tsukada:
Automated Synthesis of Functional Programs with Auxiliary Functions. APLAS 2018: 223-241 - [c20]Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
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 - [i3]Kazuyuki Asada, Naoki Kobayashi, Ryoma Sin'ya, Takeshi Tsukada:
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence. CoRR abs/1801.03886 (2018) - 2017
- [c18]Ryoma Sin'ya, Kazuyuki Asada, Naoki Kobayashi, Takeshi Tsukada:
Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence. FoSSaCS 2017: 53-68 - [c17]Ken Sakayori, Takeshi Tsukada:
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, Takeshi Tsukada:
Streett Automata Model Checking of Higher-Order Recursion Schemes. FSCD 2017: 32:1-32:18 - [i2]Naoki Kobayashi, Takeshi Tsukada, Keiichi Watanabe:
Higher-Order Program Verification via HFL Model Checking. CoRR abs/1710.08614 (2017) - 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, Ryosuke Sato, Takeshi Tsukada, Naoki Kobayashi:
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, Kazuhiro Inaba, Takeshi Tsukada:
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 - [i1]Takeshi Tsukada, C.-H. Luke Ong:
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence. CoRR abs/1409.2764 (2014) - 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, Takeshi Tsukada:
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
- [j1]Takeshi Tsukada, Atsushi Igarashi:
A Logical Foundation for Environment Classifiers. Log. Methods Comput. Sci. 6(4) (2010) - [c2]Takeshi Tsukada, Naoki Kobayashi:
Untyped Recursion Schemes and Infinite Intersection Types. FoSSaCS 2010: 343-357
2000 – 2009
- 2009
- [c1]Takeshi Tsukada, Atsushi Igarashi:
A Logical Foundation for Environment Classifiers. TLCA 2009: 341-355
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 22:08 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:
