Tsukada Takeshi 塚田武志

Researcher Number	50758951
Other IDs	https://orcid.org/0000-0002-2824-8708
Affiliation (Current)	2025: 千葉大学, 大学院理学研究院, 教授
Affiliation (based on the past Project Information) *help	2020 – 2024: 千葉大学, 大学院理学研究院, 准教授 2016 – 2020: 東京大学, 大学院情報理工学系研究科, 助教
Review Section/Research Field	Principal Investigator Basic Section 60050:Software-related / Basic Section 60010:Theory of informatics-related / Theory of informatics Except Principal Investigator Broad Section J / Medium-sized Section 60:Information science, computer engineering, and related fields
Keywords	Principal Investigator プログラム検証 / π計算 / 線形論理 / システム検証 / CHCソルバ / 定理自動証明 / 機械学習 / 演繹的推論 / Freyd圏 / 並行計算 … More / 計算効果 / η則 / 計算論的ラムダ計算 / 圏論的意味論 / 微分λ計算 / プログラム意味論 / generalised species / 交差型システム / ゲーム意味論 … More Except Principal Investigator プログラム検証 / 機械学習 / 高階不動点論理 / 高階モデル検査 / 深層学習 / 人工知能 / ホーン節ソルバ / 定理証明 / 制約付きホーン節 / 自動証明 / 強化学習 Less

機械学習技術による高速な演繹的推論エンジンの開発Principal Investigator
- Principal Investigator
  
  塚田武志
- Project Period (FY)
  2022 – 2026
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Chiba University
Program Verification Techniques for the AI Era
- Principal Investigator
  
  小林直樹
- Project Period (FY)
  2020 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (S)
- Review Section
  
  Broad Section J
- Research Institution
  The University of Tokyo
Automated Theorem Proving with Machine Learning for Automating Mathematics
- Principal Investigator
  
  Suenaga Kohei
- Project Period (FY)
  2019 – 2021
- Research Category
  
  Grant-in-Aid for Challenging Research (Exploratory)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  Kyoto University
Categorical Semantics and Logical Interpretation of the Pi-CalculusPrincipal Investigator
- Principal Investigator
  
  Tsukada Takeshi
- Project Period (FY)
  2019 – 2021
- Research Category
  
  Grant-in-Aid for Early-Career Scientists
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Chiba University
  The University of Tokyo
Game semantics and intersection type systems for program verificationPrincipal Investigator
- Principal Investigator
  
  Tsukada Takeshi
- Project Period (FY)
  2016 – 2018
- Research Category
  
  Grant-in-Aid for Young Scientists (B)
- Research Field
  
  Theory of informatics
- Research Institution
  The University of Tokyo

All 2024 2023 2022 2021 2019 2018 2017 2016

All Journal Article Presentation

[Journal Article] Optimal CHC Solving via Termination Proofs2023
- Author(s)
  Gu Yu、Tsukada Takeshi、Unno Hiroshi
- Journal Title
  
  Proceedings of the ACM on Programming Languages
  
  Volume: 7 Issue: POPL Pages: 604-631
- DOI
  10.1145/3571214
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[Journal Article] HFL(Z) Validity Checking for Automated Program Verification2023
- Author(s)
  Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada
- Journal Title
  
  Proceedings of the ACM on Programming Languages, Issue POPL, ACM
  
  Volume: 7 Issue: POPL Pages: 154-184
- DOI
  10.1145/3571199
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] Software model-checking as cyclic-proof search2022
- Author(s)
  Tsukada Takeshi、Unno Hiroshi
- Journal Title
  
  Proceedings of the ACM on Programming Languages
  
  Volume: 6 Issue: POPL Pages: 1-29
- DOI
  10.1145/3498725
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
[Journal Article] Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings2022
- Author(s)
  Takeshi Tsukada and Kazuyuki Asada
- Journal Title
  
  Proceedings of LICS 2022, ACM
  
  Volume: - Pages: 1-13
- DOI
  10.1145/3531130.3533373
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] A Cyclic Proof System for HFL_N2021
- Author(s)
  Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi
- Journal Title
  
  Proceedings of CONCUR 2021, LIPIcs
  
  Volume: 203
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] CPS transformation with affine types for call-by-value implicit polymorphism2021
- Author(s)
  Sekiyama Taro、Tsukada Takeshi
- Journal Title
  
  Proceedings of the ACM on Programming Languages (ICFP)
  
  Volume: 5 Issue: ICFP Pages: 1-30
- DOI
  10.1145/3473600
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-20H00582
[Journal Article] Output Without Delay: A Pi-Calculus Compatible with Categorical Semantics2021
- Author(s)
  Ken Sakayori and Takeshi Tsukada
- Journal Title
  
  Proceedings of FSCD 2021, LIPIcs
  
  Volume: 195
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] A Probabilistic Higher-order Fixpoint Logic2021
- Author(s)
  Mitani Yo、Kobayashi Naoki、Tsukada Takeshi
- Journal Title
  
  Logical Methods in Computer Science
  
  Volume: Volume 17, Issue 4 Pages: 1-36
- DOI
  10.46298/lmcs-17(4:15)2021
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] RustHorn: CHC-based Verification for Rust Programs2021
- Author(s)
  Matsushita Yusuke、Tsukada Takeshi、Kobayashi Naoki
- Journal Title
  
  ACM Transactions on Programming Languages and Systems
  
  Volume: 43 Issue: 4 Pages: 1-54
- DOI
  10.1145/3462205
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-22KJ0561
[Journal Article] Counterexample generation for program verification based on ownership refinement types2021
- Author(s)
  Ueno Hideto、Toman John、Kobayashi Naoki、Tsukada Takeshi
- Journal Title
  
  Proceedings of PEPM 2021, ACM Press
  
  Volume: - Pages: 44-57
- DOI
  10.1145/3441296.3441396
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] Output Without Delay: A π-Calculus Compatible with Categorical Semantics2021
- Author(s)
  Ken Sakayori, Takeshi Tsukada
- Journal Title
  
  Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction
  
  Volume: 195
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-19K20211
[Journal Article] Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination2021
- Author(s)
  Shoshi Tsubasa、Ishikawa Takuma、Kobayashi Naoki、Sakayori Ken、Sato Ryosuke、Tsukada Takeshi
- Journal Title
  
  Proceedings of APLAS 2021, Springer LNCS
  
  Volume: 13008 Pages: 265-284
- DOI
  10.1007/978-3-030-89051-3_15
- ISBN
  9783030890506, 9783030890513
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-20H05703
[Journal Article] A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus2019
- Author(s)
  Sakayori Ken、Tsukada Takeshi
- Journal Title
  
  Proceedings of the 28th European Symposium on Programming
  
  Volume: 0 Pages: 640-667
- DOI
  10.1007/978-3-030-17184-1_23
- ISBN
  9783030171834, 9783030171841
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-19K20211
[Journal Article] Species, Profunctors and Taylor Expansion Weighted by SMCC2018
- Author(s)
  Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
- Journal Title
  
  Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
  
  Volume: - Pages: 889-898
- DOI
  10.1145/3209108.3209157
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K11156, KAKENHI-PROJECT-16K16004
[Journal Article] Higher-Order Program Verification via HFL Model Checking2018
- Author(s)
  Kobayashi Naoki、Tsukada Takeshi、Watanabe Keiichi
- Journal Title
  
  Proceedings of the 27th European Symposium on Programming
  
  Volume: 0 Pages: 711-738
- DOI
  10.1007/978-3-319-89884-1_25
- ISBN
  9783319898834, 9783319898841
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[Journal Article] Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence2017
- Author(s)
  Sin’ya Ryoma, Asada Kazuyuki, Kobayashi Naoki and Tsukada Takeshi
- Journal Title
  
  Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures
  
  Volume: 0 Pages: 53-68
- DOI
  10.1007/978-3-662-54458-7_4
- ISBN
  9783662544570, 9783662544587
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[Journal Article] A Truly Concurrent Game Model of the Asynchronous Pi-Calculus2017
- Author(s)
  Ken Sakayori and Takeshi Tsukada
- Journal Title
  
  Foundations of Software Science and Computation Structures
  
  Volume: 10203 of LNCS Pages: 389-406
- DOI
  10.1007/978-3-662-54458-7_23
- ISBN
  9783662544570, 9783662544587
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K16004
[Journal Article] Verification of code generators via higher-order model checking2017
- Author(s)
  Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi and Atsushi Igarashi
- Journal Title
  
  Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation
  
  Volume: 0 Pages: 59-70
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K16004
[Journal Article] Streett Automata Model Checking of Higher-Order Recursion Schemes2017
- Author(s)
  Ryota Suzuki, Koichi Fujima, Naoki Kobayashi and Takeshi Tsukada
- Journal Title
  
  Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction
  
  Volume: 0
- DOI
  10.4230/LIPIcs.FSCD.2017.32
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[Journal Article] Generalised species of rigid resource terms2017
- Author(s)
  Takeshi Tsukada, Kazuyuki Asada and C.-H. Luke Ong
- Journal Title
  
  Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science
  
  Volume: 0 Pages: 1-12
- DOI
  10.1109/lics.2017.8005093
- Peer Reviewed / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K16004
[Journal Article] Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation2016
- Author(s)
  Kazuhide Yasukata, Takeshi Tsukada and Naoki Kobayashi
- Journal Title
  
  Programming Languages and Systems
  
  Volume: 10017 of LNCS Pages: 335-353
- DOI
  10.1007/978-3-319-47958-3_18
- ISBN
  9783319479576, 9783319479583
- Peer Reviewed / Acknowledgement Compliant
- Data Source
  KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
[Journal Article] Plays as Resource Terms via Non-idempotent Intersection Types2016
- Author(s)
  Takeshi Tsukada and C.-H. Luke Ong
- Journal Title
  
  Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science
  
  Volume: 0 Pages: 237-246
- DOI
  10.1145/2933575.2934553
- Peer Reviewed / Acknowledgement Compliant / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K16004
[Presentation] 自動検証におけるラグランジュ双対性2024
- Author(s)
  塚田武志, 海野広志
- Organizer
  第26回プログラミングおよびプログラミング言語ワークショップ
- Data Source
  KAKENHI-PROJECT-23K24820
[Presentation] Strategies in HO/N games as profunctors2016
- Author(s)
  Kazuyuki Asada and Takeshi Tsukada
- Organizer
  Games for Logic and Programming Languages XI
- Place of Presentation
  Eindhoven, The Netherlands
- Year and Date
  2016-04-02
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-16K16004

1. 関山太朗 (80828476)

# of Collaborated Projects: 3 results

# of Collaborated Products: 1 results
2. Suenaga Kohei (70633692)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
3. 海野広志 (80569575)

# of Collaborated Projects: 2 results

# of Collaborated Products: 3 results
4. 小林直樹 (00262155)

# of Collaborated Projects: 1 results

# of Collaborated Products: 6 results
5. 五十嵐淳 (40323456)

# of Collaborated Projects: 1 results

# of Collaborated Products: 1 results
6. 吉仲亮 (80466424)

# of Collaborated Projects: 1 results

# of Collaborated Products: 2 results
7. 佐藤一誠 (90610155)

# of Collaborated Projects: 1 results

# of Collaborated Products: 2 results
8. 佐藤亮介 (10804677)

# of Collaborated Projects: 1 results

# of Collaborated Products: 2 results
9. 浅田和之

# of Collaborated Projects: 0 results

# of Collaborated Products: 1 results

Tsukada Takeshi 塚田 武志

Research Projects

Research Products

Co-Researchers

機械学習技術による高速な演繹的推論エンジンの開発Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Program Verification Techniques for the AI Era

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Automated Theorem Proving with Machine Learning for Automating Mathematics

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Categorical Semantics and Logical Interpretation of the Pi-CalculusPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Game semantics and intersection type systems for program verificationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Journal Article] Optimal CHC Solving via Termination Proofs2023

Author(s)

Journal Title

DOI

Data Source

[Journal Article] HFL(Z) Validity Checking for Automated Program Verification2023

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Software model-checking as cyclic-proof search2022

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings2022

Author(s)

Journal Title

DOI

Data Source

[Journal Article] A Cyclic Proof System for HFL_N2021

Author(s)

Journal Title

Data Source

[Journal Article] CPS transformation with affine types for call-by-value implicit polymorphism2021

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Output Without Delay: A Pi-Calculus Compatible with Categorical Semantics2021

Author(s)

Journal Title

Data Source

[Journal Article] A Probabilistic Higher-order Fixpoint Logic2021

Author(s)

Journal Title

DOI

Data Source

[Journal Article] RustHorn: CHC-based Verification for Rust Programs2021

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Counterexample generation for program verification based on ownership refinement types2021

Author(s)

Journal Title

Tsukada Takeshi 塚田武志