Takeshi Tsukada

Orcid: 0000-0002-2824-8708

According to our database1, Takeshi Tsukada authored at least 50 papers between 2010 and 2024.

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

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Enriched Presheaf Model of Quantum FPC.
Proc. ACM Program. Lang., January, 2024

Inductive Approach to Spacer.
Proc. ACM Program. Lang., 2024

2023
HFL(Z) Validity Checking for Automated Program Verification.
Proc. ACM Program. Lang., January, 2023

Optimal CHC Solving via Termination Proofs.
Proc. ACM Program. Lang., January, 2023

2022
Software model-checking as cyclic-proof search.
Proc. ACM Program. Lang., 2022

Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings.
CoRR, 2022

Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱.
Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

2021
RustHorn: CHC-based Verification for Rust Programs.
ACM Trans. Program. Lang. Syst., 2021

CPS transformation with affine types for call-by-value implicit polymorphism.
Proc. ACM Program. Lang., 2021

A Probabilistic Higher-order Fixpoint Logic.
Log. Methods Comput. Sci., 2021

Termination Analysis for the π-Calculus by Reduction to Sequential Program Termination.
CoRR, 2021

Enhancing Loop-Invariant Synthesis via Reinforcement Learning.
CoRR, 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

Output Without Delay: A π-Calculus Compatible with Categorical Semantics.
Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction, 2021

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

Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination.
Proceedings of the Programming Languages and Systems - 19th Asian Symposium, 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 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


  Loading...