• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

塚田 武志  Tsukada Takeshi

研究者番号 50758951
その他のID
  • ORCIDhttps://orcid.org/0000-0002-2824-8708
所属 (現在) 2025年度: 千葉大学, 大学院理学研究院, 教授
所属 (過去の研究課題情報に基づく) *注記 2025年度: 千葉大学, 大学院理学研究院, 教授
2020年度 – 2024年度: 千葉大学, 大学院理学研究院, 准教授
2016年度 – 2020年度: 東京大学, 大学院情報理工学系研究科, 助教
審査区分/研究分野
研究代表者
小区分60050:ソフトウェア関連 / 小区分60010:情報学基礎論関連 / 情報学基礎理論
研究代表者以外
大区分J / 中区分60:情報科学、情報工学およびその関連分野
キーワード
研究代表者
プログラム検証 / π計算 / 線形論理 / システム検証 / CHCソルバ / 定理自動証明 / 機械学習 / 演繹的推論 / Freyd圏 / 並行計算 … もっと見る / 計算効果 / η則 / 計算論的ラムダ計算 / 圏論的意味論 / 微分λ計算 / プログラム意味論 / generalised species / 交差型システム / ゲーム意味論 … もっと見る
研究代表者以外
プログラム検証 / 機械学習 / 学習理論 / 最適化理論 / 計算論 / 論理学 / 高階不動点論理 / 高階モデル検査 / 深層学習 / 人工知能 / ホーン節ソルバ / 定理証明 / 制約付きホーン節 / 自動証明 / 強化学習 隠す
  • 研究課題

    (6件)
  • 研究成果

    (24件)
  • 共同研究者

    (12人)
  •  プログラム検証技術の基礎付けと応用

    • 研究代表者
      海野 広志
    • 研究期間 (年度)
      2025 – 2029
    • 研究種目
      基盤研究(S)
    • 審査区分
      大区分J
    • 研究機関
      東北大学
  •  機械学習技術による高速な演繹的推論エンジンの開発研究代表者

    • 研究代表者
      塚田 武志
    • 研究期間 (年度)
      2022 – 2026
    • 研究種目
      基盤研究(B)
    • 審査区分
      小区分60050:ソフトウェア関連
    • 研究機関
      千葉大学
  •  AI時代を見据えたプログラム検証技術

    • 研究代表者
      小林 直樹
    • 研究期間 (年度)
      2020 – 2024
    • 研究種目
      基盤研究(S)
    • 審査区分
      大区分J
    • 研究機関
      東京大学
  •  数学の自動化を推進するための機械学習を用いた定理自動証明手法

    • 研究代表者
      末永 幸平
    • 研究期間 (年度)
      2019 – 2021
    • 研究種目
      挑戦的研究(萌芽)
    • 審査区分
      中区分60:情報科学、情報工学およびその関連分野
    • 研究機関
      京都大学
  •  π計算の圏論的意味論と論理的解釈研究代表者

    • 研究代表者
      塚田 武志
    • 研究期間 (年度)
      2019 – 2021
    • 研究種目
      若手研究
    • 審査区分
      小区分60010:情報学基礎論関連
    • 研究機関
      千葉大学
      東京大学
  •  ゲーム意味論と交差型システムによるプログラム検証研究代表者

    • 研究代表者
      塚田 武志
    • 研究期間 (年度)
      2016 – 2018
    • 研究種目
      若手研究(B)
    • 研究分野
      情報学基礎理論
    • 研究機関
      東京大学

すべて 2024 2023 2022 2021 2019 2018 2017 2016

すべて 雑誌論文 学会発表

  • [雑誌論文] Optimal CHC Solving via Termination Proofs2023

    • 著者名/発表者名
      Gu Yu、Tsukada Takeshi、Unno Hiroshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 7 号: POPL ページ: 604-631

    • DOI

      10.1145/3571214

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-23K24820, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] HFL(Z) Validity Checking for Automated Program Verification2023

    • 著者名/発表者名
      Naoki Kobayashi, Kento Tanahashi, Ryosuke Sato, and Takeshi Tsukada
    • 雑誌名

      Proceedings of the ACM on Programming Languages, Issue POPL, ACM

      巻: 7 号: POPL ページ: 154-184

    • DOI

      10.1145/3571199

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] Software model-checking as cyclic-proof search2022

    • 著者名/発表者名
      Tsukada Takeshi、Unno Hiroshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages

      巻: 6 号: POPL ページ: 1-29

    • DOI

      10.1145/3498725

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-23K20380
  • [雑誌論文] Linear-Algebraic Models of Linear Logic as Categories of Modules over Sigma-Semirings2022

    • 著者名/発表者名
      Takeshi Tsukada and Kazuyuki Asada
    • 雑誌名

      Proceedings of LICS 2022, ACM

      巻: - ページ: 1-13

    • DOI

      10.1145/3531130.3533373

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] A Cyclic Proof System for HFL_N2021

    • 著者名/発表者名
      Mayuko Kori, Takeshi Tsukada, and Naoki Kobayashi
    • 雑誌名

      Proceedings of CONCUR 2021, LIPIcs

      巻: 203

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] CPS transformation with affine types for call-by-value implicit polymorphism2021

    • 著者名/発表者名
      Sekiyama Taro、Tsukada Takeshi
    • 雑誌名

      Proceedings of the ACM on Programming Languages (ICFP)

      巻: 5 号: ICFP ページ: 1-30

    • DOI

      10.1145/3473600

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-19K20247, KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-20H00582
  • [雑誌論文] Output Without Delay: A Pi-Calculus Compatible with Categorical Semantics2021

    • 著者名/発表者名
      Ken Sakayori and Takeshi Tsukada
    • 雑誌名

      Proceedings of FSCD 2021, LIPIcs

      巻: 195

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] A Probabilistic Higher-order Fixpoint Logic2021

    • 著者名/発表者名
      Mitani Yo、Kobayashi Naoki、Tsukada Takeshi
    • 雑誌名

      Logical Methods in Computer Science

      巻: Volume 17, Issue 4 ページ: 1-36

    • DOI

      10.46298/lmcs-17(4:15)2021

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] RustHorn: CHC-based Verification for Rust Programs2021

    • 著者名/発表者名
      Matsushita Yusuke、Tsukada Takeshi、Kobayashi Naoki
    • 雑誌名

      ACM Transactions on Programming Languages and Systems

      巻: 43 号: 4 ページ: 1-54

    • DOI

      10.1145/3462205

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-20H05703, KAKENHI-PROJECT-22KJ0561
  • [雑誌論文] Counterexample generation for program verification based on ownership refinement types2021

    • 著者名/発表者名
      Ueno Hideto、Toman John、Kobayashi Naoki、Tsukada Takeshi
    • 雑誌名

      Proceedings of PEPM 2021, ACM Press

      巻: - ページ: 44-57

    • DOI

      10.1145/3441296.3441396

    • 査読あり
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] Output Without Delay: A π-Calculus Compatible with Categorical Semantics2021

    • 著者名/発表者名
      Ken Sakayori, Takeshi Tsukada
    • 雑誌名

      Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction

      巻: 195

    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-19K20211
  • [雑誌論文] Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination2021

    • 著者名/発表者名
      Shoshi Tsubasa、Ishikawa Takuma、Kobayashi Naoki、Sakayori Ken、Sato Ryosuke、Tsukada Takeshi
    • 雑誌名

      Proceedings of APLAS 2021, Springer LNCS

      巻: 13008 ページ: 265-284

    • DOI

      10.1007/978-3-030-89051-3_15

    • ISBN
      9783030890506, 9783030890513
    • 査読あり
    • データソース
      KAKENHI-PROJECT-20H05703
  • [雑誌論文] A Categorical Model of an $$\mathbf {i/o}$$ -typed $$\pi $$ -calculus2019

    • 著者名/発表者名
      Sakayori Ken、Tsukada Takeshi
    • 雑誌名

      Proceedings of the 28th European Symposium on Programming

      巻: 0 ページ: 640-667

    • DOI

      10.1007/978-3-030-17184-1_23

    • ISBN
      9783030171834, 9783030171841
    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-19K20211
  • [雑誌論文] Species, Profunctors and Taylor Expansion Weighted by SMCC2018

    • 著者名/発表者名
      Takeshi Tsukada, Kazuyuki Asada, C.-H. Luke Ong
    • 雑誌名

      Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

      巻: - ページ: 889-898

    • DOI

      10.1145/3209108.3209157

    • 査読あり / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-18K11156, KAKENHI-PROJECT-16K16004
  • [雑誌論文] Higher-Order Program Verification via HFL Model Checking2018

    • 著者名/発表者名
      Kobayashi Naoki、Tsukada Takeshi、Watanabe Keiichi
    • 雑誌名

      Proceedings of the 27th European Symposium on Programming

      巻: 0 ページ: 711-738

    • DOI

      10.1007/978-3-319-89884-1_25

    • ISBN
      9783319898834, 9783319898841
    • 査読あり / オープンアクセス
    • データソース
      KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
  • [雑誌論文] Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence2017

    • 著者名/発表者名
      Sin’ya Ryoma, Asada Kazuyuki, Kobayashi Naoki and Tsukada Takeshi
    • 雑誌名

      Proceedings of the 20th International Conference on Foundations of Software Science and Computation Structures

      巻: 0 ページ: 53-68

    • DOI

      10.1007/978-3-662-54458-7_4

    • ISBN
      9783662544570, 9783662544587
    • 査読あり
    • データソース
      KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
  • [雑誌論文] A Truly Concurrent Game Model of the Asynchronous Pi-Calculus2017

    • 著者名/発表者名
      Ken Sakayori and Takeshi Tsukada
    • 雑誌名

      Foundations of Software Science and Computation Structures

      巻: 10203 of LNCS ページ: 389-406

    • DOI

      10.1007/978-3-662-54458-7_23

    • ISBN
      9783662544570, 9783662544587
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-16K16004
  • [雑誌論文] Verification of code generators via higher-order model checking2017

    • 著者名/発表者名
      Takashi Suwa, Takeshi Tsukada, Naoki Kobayashi and Atsushi Igarashi
    • 雑誌名

      Proceedings of the 2017 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

      巻: 0 ページ: 59-70

    • 査読あり
    • データソース
      KAKENHI-PROJECT-16K16004
  • [雑誌論文] Streett Automata Model Checking of Higher-Order Recursion Schemes2017

    • 著者名/発表者名
      Ryota Suzuki, Koichi Fujima, Naoki Kobayashi and Takeshi Tsukada
    • 雑誌名

      Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction

      巻: 0

    • DOI

      10.4230/LIPIcs.FSCD.2017.32

    • 査読あり
    • データソース
      KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
  • [雑誌論文] Generalised species of rigid resource terms2017

    • 著者名/発表者名
      Takeshi Tsukada, Kazuyuki Asada and C.-H. Luke Ong
    • 雑誌名

      Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science

      巻: 0 ページ: 1-12

    • DOI

      10.1109/lics.2017.8005093

    • 査読あり / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16K16004
  • [雑誌論文] Verification of Higher-Order Concurrent Programs with Dynamic Resource Creation2016

    • 著者名/発表者名
      Kazuhide Yasukata, Takeshi Tsukada and Naoki Kobayashi
    • 雑誌名

      Programming Languages and Systems

      巻: 10017 of LNCS ページ: 335-353

    • DOI

      10.1007/978-3-319-47958-3_18

    • ISBN
      9783319479576, 9783319479583
    • 査読あり / 謝辞記載あり
    • データソース
      KAKENHI-PROJECT-16K16004, KAKENHI-PROJECT-15H05706
  • [雑誌論文] Plays as Resource Terms via Non-idempotent Intersection Types2016

    • 著者名/発表者名
      Takeshi Tsukada and C.-H. Luke Ong
    • 雑誌名

      Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science

      巻: 0 ページ: 237-246

    • DOI

      10.1145/2933575.2934553

    • 査読あり / 謝辞記載あり / 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16K16004
  • [学会発表] 自動検証におけるラグランジュ双対性2024

    • 著者名/発表者名
      塚田 武志, 海野 広志
    • 学会等名
      第26回プログラミングおよびプログラミング言語ワークショップ
    • データソース
      KAKENHI-PROJECT-23K24820
  • [学会発表] Strategies in HO/N games as profunctors2016

    • 著者名/発表者名
      Kazuyuki Asada and Takeshi Tsukada
    • 学会等名
      Games for Logic and Programming Languages XI
    • 発表場所
      Eindhoven, The Netherlands
    • 年月日
      2016-04-02
    • 国際共著/国際学会である
    • データソース
      KAKENHI-PROJECT-16K16004
  • 1.  関山 太朗 (80828476)
    共同の研究課題数: 3件
    共同の研究成果数: 1件
  • 2.  海野 広志 (80569575)
    共同の研究課題数: 3件
    共同の研究成果数: 3件
  • 3.  末永 幸平 (70633692)
    共同の研究課題数: 2件
    共同の研究成果数: 0件
  • 4.  小林 直樹 (00262155)
    共同の研究課題数: 1件
    共同の研究成果数: 6件
  • 5.  五十嵐 淳 (40323456)
    共同の研究課題数: 1件
    共同の研究成果数: 1件
  • 6.  吉仲 亮 (80466424)
    共同の研究課題数: 1件
    共同の研究成果数: 2件
  • 7.  佐藤 一誠 (90610155)
    共同の研究課題数: 1件
    共同の研究成果数: 2件
  • 8.  佐藤 亮介 (10804677)
    共同の研究課題数: 1件
    共同の研究成果数: 2件
  • 9.  内藏 理史 (10969364)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 10.  川島 英之 (90407148)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 11.  龍田 真 (80216994)
    共同の研究課題数: 1件
    共同の研究成果数: 0件
  • 12.  浅田 和之
    共同の研究課題数: 0件
    共同の研究成果数: 1件

URL: 

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi