According to our database1, Takeshi Tsukada authored at least 38 papers between 2010 and 2021.

Collaborative distances:
• Dijkstra number2 of four.
• Erdős number3 of four.

Book
In proceedings
Article
PhD thesis
Other

## Bibliography

2021
Counterexample generation for program verification based on ownership refinement types.
Proceedings of the 2021 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2021

A Cyclic Proof System for HFL_ℕ.
Proceedings of the 29th EACSL Annual Conference on Computer Science Logic, 2021

2020
Signature restriction for polymorphic algebraic effects.
Proc. ACM Program. Lang., 2020

A Cyclic Proof System for HFLN.
CoRR, 2020

RustHorn: CHC-based Verification for Rust Programs (full version).
CoRR, 2020

Predicate Abstraction and CEGAR for $\nu \mathrm {HFL}_\mathbb {Z}$ Validity Checking.
Proceedings of the Static Analysis - 27th International Symposium, 2020

On Computability of Logical Approaches to Branching-Time Property Verification of Programs.
Proceedings of the LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, 2020

On Average-Case Hardness of Higher-Order Model Checking.
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

A Probabilistic Higher-Order Fixpoint Logic.
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

RustHorn: CHC-Based Verification for Rust Programs.
Proceedings of the Programming Languages and Systems, 2020

A New Refinement Type System for Automated $\nu \text {HFL}_\mathbb {Z}$ Validity Checking.
Proceedings of the Programming Languages and Systems - 18th Asian Symposium, 2020

2019
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence.
Log. Methods Comput. Sci., 2019

A Temporal Logic for Higher-Order Functional Programs.
Proceedings of the Static Analysis - 26th International Symposium, 2019

Reduction from branching-time property verification of higher-order programs to HFL validity checking.
Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2019

A Categorical Model of an \mathbf i/o -typed \pi -calculus.
Proceedings of the Programming Languages and Systems, 2019

A Type-Based HFL Model Checking Algorithm.
Proceedings of the Programming Languages and Systems - 17th Asian Symposium, 2019

2018
Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Higher-Order Program Verification via HFL Model Checking.
Proceedings of the Programming Languages and Systems, 2018

Automated Synthesis of Functional Programs with Auxiliary Functions.
Proceedings of the Programming Languages and Systems - 16th Asian Symposium, 2018

2017
Streett Automata Model Checking of Higher-Order Recursion Schemes.
Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction, 2017

Verification of code generators via higher-order model checking.
Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 2017

Generalised species of rigid resource terms.
Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, 2017

Almost Every Simply Typed λ-Term Has a Long β-Reduction Sequence.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

A Truly Concurrent Game Model of the Asynchronous \pi -Calculus.
Proceedings of the Foundations of Software Science and Computation Structures, 2017

2016
Plays as Resource Terms via Non-idempotent Intersection Types.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

Automatically disproving fair termination of higher-order functional programs.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

Higher-Order Model Checking in Direct Style.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015
Nondeterminism in Game Semantics via Sheaves.
Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, 2015

2014
Innocent Strategies are Sheaves over Plays - Deterministic, Non-deterministic and Probabilistic Innocence.
CoRR, 2014

Complexity of Model-Checking Call-by-Value Programs.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Unsafe Order-2 Tree Languages Are Context-Sensitive.
Proceedings of the Foundations of Software Science and Computation Structures, 2014

Compositional higher-order model checking via <i>ω</i>-regular games over Böhm trees.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

2012
An Intersection Type System for Deterministic Pushdown Automata.
Proceedings of the Theoretical Computer Science, 2012

Two-Level Game Semantics, Intersection Types, and Recursion Schemes.
Proceedings of the Automata, Languages, and Programming - 39th International Colloquium, 2012

Exact Flow Analysis by Higher-Order Model Checking.
Proceedings of the Functional and Logic Programming - 11th International Symposium, 2012

2010
A Logical Foundation for Environment Classifiers
Log. Methods Comput. Sci., 2010

Untyped Recursion Schemes and Infinite Intersection Types.
Proceedings of the Foundations of Software Science and Computational Structures, 2010