才川隆文 Saikawa Takafumi

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

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

すべて 2023 2022

すべて雑誌論文学会発表

[雑誌論文] 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
[学会発表] OCaml プログラムの Coq への変換とプログラムの正しさの証明2023
- 著者名/発表者名
  毎田詠人, 中村薫, 才川隆文, Jacques Garrigue
- 学会等名
  プログラミングおよびプログラミング言語研究会
- データソース
  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
- 国際共著/国際学会である
- データソース
  KAKENHI-PROJECT-22H00520
[学会発表] Environment-Friendly Monadic Equational Reasoning for OCaml2023
- 著者名/発表者名
  Takafumi Saikawa
- 学会等名
  Coq Workshop 2023
- 国際共著/国際学会である
- データソース
  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
[学会発表] OCaml から Coq へのコンパイラ及び翻訳されたプログラムの証明2022
- 著者名/発表者名
  中村薫, 才川隆文, Jacques Garrigue, 毎田詠人
- 学会等名
  日本ソフトウェア科学会全国大会
- データソース
  KAKENHI-PROJECT-22K11902
[学会発表] 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件

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

共同の研究課題数: 2件

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

共同の研究課題数: 1件

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

共同の研究課題数: 1件

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

共同の研究課題数: 1件

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

共同の研究課題数: 1件

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

共同の研究課題数: 0件

共同の研究成果数: 8件

才川 隆文 Saikawa Takafumi

研究課題

研究成果

共同研究者

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

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

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

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

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

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

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

研究代表者

研究期間 (年度)

研究種目

審査区分

研究機関

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

著者名/発表者名

雑誌名

データソース

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

著者名/発表者名

雑誌名

データソース

[学会発表] OCaml プログラムの Coq への変換とプログラムの正しさの証明2023

著者名/発表者名

学会等名

データソース

[学会発表] Environment-friendly monadic equational reasoning for OCaml2023

著者名/発表者名

学会等名

データソース

[学会発表] Environment-Friendly Monadic Equational Reasoning for OCaml2023

著者名/発表者名

学会等名

データソース

[学会発表] Validating OCaml soundness by translation into Coq2022

著者名/発表者名

学会等名

データソース

[学会発表] Formalizing quantum circuits with mathcomp/ssreflect (Poster)2022

著者名/発表者名

学会等名

データソース

[学会発表] OCaml から Coq へのコンパイラ及び翻訳されたプログラムの証明2022

著者名/発表者名

学会等名

データソース

[学会発表] Interpreting OCaml GADTs into Coq2022

著者名/発表者名

学会等名

データソース

才川隆文 Saikawa Takafumi