• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Tsukada Takeshi  塚田 武志

Researcher Number 50758951
Other IDs
  • ORCIDhttps://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
  • Research Projects

    (5 results)
  • Research Products

    (24 results)
  • Co-Researchers

    (9 People)
  •  機械学習技術による高速な演繹的推論エンジンの開発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

URL: 

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi