才川隆文 Saikawa Takafumi

研究者番号	00897100
その他のID	https://orcid.org/0000-0003-4492-745X
所属 (現在)	2026年度: 名古屋大学, 多元数理科学研究科, 特任助教
所属 (過去の研究課題情報に基づく) *注記	2022年度 – 2025年度: 名古屋大学, 多元数理科学研究科, 研究員
審査区分/研究分野	研究代表者小区分60010:情報学基礎論関連研究代表者以外小区分60050:ソフトウェア関連 / 中区分60:情報科学、情報工学およびその関連分野 / 小区分60010:情報学基礎論関連
キーワード	研究代表者型理論 / 可換代数 / 定理証明支援系 / MathComp / Coq / Rocq / マッチング数 / グラフ理論 / 数学の形式化研究代表者以外等式理論 … もっと見る / 定理証明支援系 / 計算効果 / 関数型プログラミング言語 / プログラム検証 / 確率的プログラミング / Coq / 数学の形式化 / 形式検証 / 形式的証明 / 依存型 / コンパイラー / 型システム / 操作的意味論 / 型推論 / 双模倣 / 相模倣 / 非停止性 / 参照型 / プログラムの証明 / 型健全性隠す

計算効果を持つプログラムの証明のための枠組みの構築
- 研究代表者
  
  J Garrigue
- 研究期間 (年度)
  2025 – 2028
- 研究種目
  
  基盤研究(B)
- 審査区分
  
  小区分60050:ソフトウェア関連
- 研究機関
  名古屋大学
定理証明支援系を用いた数学的定理の発見的証明研究代表者
- 研究代表者
  
  才川隆文
- 研究期間 (年度)
  2024 – 2026
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
論理体系への翻訳によるプログラミング言語の型健全性の保証
- 研究代表者
  
  J Garrigue
- 研究期間 (年度)
  2022 – 2024
- 研究種目
  
  基盤研究(C)
- 審査区分
  
  小区分60010:情報学基礎論関連
- 研究機関
  名古屋大学
物理的・確率的システムの検証を支える形式的基盤の構築
- 研究代表者
  
  Affeldt Reynald
- 研究期間 (年度)
  2022 – 2025
- 研究種目
  
  基盤研究(A)
- 審査区分
  
  中区分60:情報科学、情報工学およびその関連分野
- 研究機関
  国立研究開発法人産業技術総合研究所

すべて 2025 2024 2023 2022

すべて雑誌論文学会発表

[雑誌論文] モナド等式変形による while 文の形式検証2025
- 著者名/発表者名
  川上竜司, Jacques Garrigue, 才川隆文, Reynald Affeldt
- 雑誌名
  
  第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
  
  巻: 1
- 査読あり
- データソース
  KAKENHI-PROJECT-22H00520
[雑誌論文] A practical formalization of monadic equational reasoning in dependent-type theory2025
- 著者名/発表者名
  Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 雑誌名
  
  Journal of Functional Programming
  
  巻: 35 ページ: 1-40
- DOI
  10.1017/s0956796824000157
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-22H00520, KAKENHI-PROJECT-22K11902
[雑誌論文] Toward a Formalization of Secure Multiparty Computation Stack2025
- 著者名/発表者名
  Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 雑誌名
  
  第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
  
  巻: 1
- 査読あり
- データソース
  KAKENHI-PROJECT-22H00520
[雑誌論文] Typed Compositional Quantum Computation with Lenses2024
- 著者名/発表者名
  Jacques Garrigue, Takafumi Saikawa
- 雑誌名
  
  15th International Conference on Interactive Theorem Proving (ITP 2024), September 9-14, 2024, Tbilisi, Georgia, Leibniz International Proceedings in Informatics
  
  巻: 309
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-22H00520
[雑誌論文] Robust Mean Estimation by All Means (Short Paper)2024
- 著者名/発表者名
  Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schurmann
- 雑誌名
  
  15th International Conference on Interactive Theorem Proving (ITP 2024), September 9-14, 2024, Tbilisi, Georgia, Leibniz International Proceedings in Informatics
  
  巻: 309
- 査読あり / オープンアクセス / 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[雑誌論文] A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory2023
- 著者名/発表者名
  Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 雑誌名
  
  arXiv
  
  巻: 2312 ページ: 1-38
- オープンアクセス
- データソース
  KAKENHI-PROJECT-22K11902
[雑誌論文] Environment-friendly monadic equational reasoning for OCaml2023
- 著者名/発表者名
  Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 雑誌名
  
  The Coq Workshop 2023, Bialystok, Poland, July 31, 2023
  
  巻: 1
- 査読あり / オープンアクセス
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] モナド等式変形によるwhile 文の形式検証2025
- 著者名/発表者名
  川上竜司, Jacques Garrigue, 才川隆文, Reynald Affeldt
- 学会等名
  第27回プログラミングおよびプログラミング言語ワークショップ (PPL 2025)
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] Complete graphs and independence numbers2024
- 著者名/発表者名
  Takafumi Saikawa
- 学会等名
  Theorem Proving and Provers 2024 (TPP2024), 九州大学マス・フォア・インダストリ研究所共同利用研究集会コンピュータによる定理証明支援とその応用
- データソース
  KAKENHI-PROJECT-24K14820
[学会発表] 遅延モナドを用いた一般再帰関数に対する等式変形による検証2024
- 著者名/発表者名
  Ryuji Kawakami, Jacques Garrigue, Takahumi Saikawa, Reynald Affeldt
- 学会等名
  第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Mechanized monadic equational reasoning for ML references2024
- 著者名/発表者名
  Jacques Garrigue, Reynald Affeldt, Takafumi Saikawa
- 学会等名
  12th ACM SIGPLAN Workshop on Higher-Order Programming with Effects (HOPE 2024)
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] Robust mean estimation by all means (short paper)2024
- 著者名/発表者名
  Reynald Affeldt, Clark Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schurmann
- 学会等名
  5th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia, September 9-14, 2024
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Developing probability theory using the Lebesgue integral in Coq2024
- 著者名/発表者名
  Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa
- 学会等名
  第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Toward a Formalization of Secure-Multiparty Computation Stack2024
- 著者名/発表者名
  Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 学会等名
  第27回プログラミングおよびプログラミング言語ワークショップ（PPL 2025）
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Typed Compositional Quantum Computation with Lenses2024
- 著者名/発表者名
  Jacques Garrigue, Takafumi Saikawa
- 学会等名
  5th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia, September 9-14, 2024
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Environment-friendly monadic equational reasoning for OCaml2023
- 著者名/発表者名
  Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
- 学会等名
  The Coq Workshop 2023, Bialystok, Poland, July 31, 2023
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] OCaml プログラムの Coq への変換とプログラムの正しさの証明2023
- 著者名/発表者名
  毎田詠人, 中村薫, 才川隆文, Jacques Garrigue
- 学会等名
  プログラミングおよびプログラミング言語研究会
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] Environment-Friendly Monadic Equational Reasoning for OCaml2023
- 著者名/発表者名
  Takafumi Saikawa
- 学会等名
  Coq Workshop 2023
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] OCaml から Coq へのコンパイラ及び翻訳されたプログラムの証明2022
- 著者名/発表者名
  中村薫, 才川隆文, Jacques Garrigue, 毎田詠人
- 学会等名
  日本ソフトウェア科学会全国大会
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] Validating OCaml soundness by translation into Coq2022
- 著者名/発表者名
  Takafumi Saikawa, Jacques Garrigue
- 学会等名
  TYPES
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] Formalizing quantum circuits with mathcomp/ssreflect (Poster)2022
- 著者名/発表者名
  Jacques Garrigue, Takafumi Saikawa
- 学会等名
  PlanQC 2022, Ljubljana, Slovenia
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Interpreting OCaml GADTs into Coq2022
- 著者名/発表者名
  Jacques Garrigue, Takafumi Saikawa
- 学会等名
  ML Workshop
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22K11902

1. J Garrigue (80273530)

共同の研究課題数: 3件

共同の研究成果数: 0件
2. Affeldt Reynald (40415641)

共同の研究課題数: 3件

共同の研究成果数: 13件
3. 勝股審也 (30378963)

共同の研究課題数: 2件

共同の研究成果数: 0件
4. 中野圭介 (30505839)

共同の研究課題数: 1件

共同の研究成果数: 0件
5. 溝口佳寛 (80209783)

共同の研究課題数: 1件

共同の研究成果数: 0件
6. 田中哲 (10357452)

共同の研究課題数: 1件

共同の研究成果数: 0件
7. 松田一徳 (20633241)

共同の研究課題数: 1件

共同の研究成果数: 0件
8. GAARUGUE Jacques

共同の研究課題数: 0件

共同の研究成果数: 17件

才川 隆文 Saikawa Takafumi

研究課題

研究成果

共同研究者

計算効果を持つプログラムの証明のための枠組みの構築

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

定理証明支援系を用いた数学的定理の発見的証明研究代表者

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

論理体系への翻訳によるプログラミング言語の型健全性の保証

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

物理的・確率的システムの検証を支える形式的基盤の構築

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

[雑誌論文] モナド等式変形による while 文の形式検証2025

著者名/発表者名

雑誌名

データソース

[雑誌論文] A practical formalization of monadic equational reasoning in dependent-type theory2025

著者名/発表者名

雑誌名

DOI

データソース

[雑誌論文] Toward a Formalization of Secure Multiparty Computation Stack2025

著者名/発表者名

雑誌名

データソース

[雑誌論文] Typed Compositional Quantum Computation with Lenses2024

著者名/発表者名

雑誌名

データソース

[雑誌論文] Robust Mean Estimation by All Means (Short Paper)2024

著者名/発表者名

雑誌名

データソース

[雑誌論文] A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory2023

著者名/発表者名

雑誌名

データソース

[雑誌論文] Environment-friendly monadic equational reasoning for OCaml2023

著者名/発表者名

雑誌名

データソース

[学会発表] モナド等式変形によるwhile 文の形式検証2025

著者名/発表者名

学会等名

データソース

[学会発表] Complete graphs and independence numbers2024

著者名/発表者名

学会等名

データソース

[学会発表] 遅延モナドを用いた一般再帰関数に対する等式変形による検証2024

著者名/発表者名

学会等名

データソース

[学会発表] Mechanized monadic equational reasoning for ML references2024

著者名/発表者名

学会等名

データソース

[学会発表] Robust mean estimation by all means (short paper)2024

著者名/発表者名

学会等名

データソース

[学会発表] Developing probability theory using the Lebesgue integral in Coq2024

著者名/発表者名

学会等名

才川隆文 Saikawa Takafumi