Research keywords (4):
program verification
, type system
, game semantics
, semantics of programs
Research theme for competitive and other funds (6):
2022 - 2027 機械学習技術による高速な演繹的推論エンジンの開発
2020 - 2025 Program Verification Techniques for the AI Era
2019 - 2022 Automated Theorem Proving with Machine Learning for Automating Mathematics
2019 - 2022 Categorical Semantics and Logical Interpretation of the Pi-Calculus
2016 - 2019 Game semantics and intersection type systems for program verification
2010 - 2012 高階再帰スキームのモデル検査とそのプログラム検証への応用
Show all
Papers (47):
Takeshi Tsukada, Kazuyuki Asada. Enriched Presheaf Model of Quantum FPC. Proceedings of the ACM on Programming Languages. 2024
Yu Gu, Takeshi Tsukada, Hiroshi Unno. Optimal CHC Solving via Termination Proofs. Proc. ACM Program. Lang. 2023. 7. POPL. 604-631
Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, Takeshi Tsukada. HFL(Z) Validity Checking for Automated Program Verification. Proc. ACM Program. Lang. 2023. 7. POPL. 154-184
Takeshi Tsukada, Hiroshi Unno. Software model-checking as cyclic-proof search. Proceedings of the ACM on Programming Languages. 2022. 6. POPL. 1-29
Takeshi Tsukada, Kazuyuki Asada. Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings. Proceedings of 27th Annual ACM/IEEE Symposium on Logic in Computer Science (LiCS 2022). 2022. 60-13