Saikawa Takafumi 才川隆文

Researcher Number	00897100
Other IDs	https://orcid.org/0000-0003-4492-745X
Affiliation (Current)	2025: 名古屋大学, 多元数理科学研究科, 特任助教
Affiliation (based on the past Project Information) *help	2022 – 2025: 名古屋大学, 多元数理科学研究科, 研究員
Review Section/Research Field	Principal Investigator Basic Section 60010:Theory of informatics-related Except Principal Investigator Basic Section 60050:Software-related / Medium-sized Section 60:Information science, computer engineering, and related fields / Basic Section 60010:Theory of informatics-related
Keywords	Principal Investigator 型理論 / 可換代数 / 定理証明支援系 / MathComp / Coq / Rocq / マッチング数 / グラフ理論 / 数学の形式化 Except Principal Investigator 等式理論 … More / 定理証明支援系 / 計算効果 / 関数型プログラミング言語 / プログラム検証 / 確率的プログラミング / Coq / 数学の形式化 / 形式検証 / 形式的証明 / 依存型 / コンパイラー / 型システム / 操作的意味論 / 型推論 / 双模倣 / 相模倣 / 非停止性 / 参照型 / プログラムの証明 / 型健全性 Less

Construction of a framework for proving the correctness of program using computational effects
- Principal Investigator
  
  J Garrigue
- Project Period (FY)
  2025 – 2028
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Nagoya University
Application of Proof Assistants to the Exploration for Novel Mathematical TheoremsPrincipal Investigator
- Principal Investigator
  
  才川隆文
- Project Period (FY)
  2024 – 2026
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
Validating the type soundness of a programming language through translation into a logical system
- Principal Investigator
  
  Garrigue Jacques
- Project Period (FY)
  2022 – 2024
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60010:Theory of informatics-related
- Research Institution
  Nagoya University
Formal Foundations for Verification of Physical and Probabilistic Systems
- Principal Investigator
  
  Affeldt Reynald
- Project Period (FY)
  2022 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (A)
- Review Section
  
  Medium-sized Section 60:Information science, computer engineering, and related fields
- Research Institution
  National Institute of Advanced Industrial Science and Technology

All 2025 2024 2023 2022

All Journal Article Presentation

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

1. Garrigue Jacques (80273530)

# of Collaborated Projects: 3 results

# of Collaborated Products: 0 results
2. Affeldt Reynald (40415641)

# of Collaborated Projects: 3 results

# of Collaborated Products: 13 results
3. 勝股審也 (30378963)

# of Collaborated Projects: 2 results

# of Collaborated Products: 0 results
4. 中野圭介 (30505839)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
5. 溝口佳寛 (80209783)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
6. 田中哲 (10357452)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
7. 松田一徳 (20633241)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
8. GAARUGUE Jacques

# of Collaborated Projects: 0 results

# of Collaborated Products: 17 results

Saikawa Takafumi 才川 隆文

Research Projects

Research Products

Co-Researchers

Construction of a framework for proving the correctness of program using computational effects

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Application of Proof Assistants to the Exploration for Novel Mathematical TheoremsPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Validating the type soundness of a programming language through translation into a logical system

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Formal Foundations for Verification of Physical and Probabilistic Systems

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

[Journal Article] モナド等式変形による while 文の形式検証2025

Author(s)

Journal Title

Data Source

[Journal Article] A practical formalization of monadic equational reasoning in dependent-type theory2025

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Toward a Formalization of Secure Multiparty Computation Stack2025

Author(s)

Journal Title

Data Source

[Journal Article] Typed Compositional Quantum Computation with Lenses2024

Author(s)

Journal Title

Data Source

[Journal Article] Robust Mean Estimation by All Means (Short Paper)2024

Author(s)

Journal Title

Data Source

[Journal Article] A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory2023

Author(s)

Journal Title

Data Source

[Journal Article] Environment-friendly monadic equational reasoning for OCaml2023

Author(s)

Journal Title

Data Source

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

Author(s)

Organizer

Data Source

[Presentation] Complete graphs and independence numbers2024

Author(s)

Organizer

Data Source

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

Author(s)

Organizer

Data Source

[Presentation] Mechanized monadic equational reasoning for ML references2024

Author(s)

Organizer

Data Source

[Presentation] Robust mean estimation by all means (short paper)2024

Author(s)

Organizer

Data Source

[Presentation] Developing probability theory using the Lebesgue integral in Coq2024

Author(s)

Organizer

Saikawa Takafumi 才川隆文