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 型理論 / 可換代数 / グラフ理論 / Coq / 定理証明支援系 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
  
  J Garrigue
- 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 2023 2022

All Journal Article Presentation

[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] OCaml プログラムの Coq への変換とプログラムの正しさの証明2023
- Author(s)
  毎田詠人, 中村薫, 才川隆文, Jacques Garrigue
- Organizer
  プログラミングおよびプログラミング言語研究会
- Data Source
  KAKENHI-PROJECT-22K11902
[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] 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] 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] OCaml から Coq へのコンパイラ及び翻訳されたプログラムの証明2022
- Author(s)
  中村薫, 才川隆文, Jacques Garrigue, 毎田詠人
- Organizer
  日本ソフトウェア科学会全国大会
- Data Source
  KAKENHI-PROJECT-22K11902
[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. J Garrigue (80273530)

# of Collaborated Projects: 3 results

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

# of Collaborated Projects: 3 results

# of Collaborated Products: 3 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. 松田一徳 (20633241)

# of Collaborated Projects: 1 results

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

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
8. GAARUGUE Jacques

# of Collaborated Projects: 0 results

# of Collaborated Products: 8 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] 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] OCaml プログラムの Coq への変換とプログラムの正しさの証明2023

Author(s)

Organizer

Data Source

[Presentation] Environment-friendly monadic equational reasoning for OCaml2023

Author(s)

Organizer

Data Source

[Presentation] Environment-Friendly Monadic Equational Reasoning for OCaml2023

Author(s)

Organizer

Data Source

[Presentation] Validating OCaml soundness by translation into Coq2022

Author(s)

Organizer

Data Source

[Presentation] Formalizing quantum circuits with mathcomp/ssreflect (Poster)2022

Author(s)

Organizer

Data Source

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

Author(s)

Organizer

Data Source

[Presentation] Interpreting OCaml GADTs into Coq2022

Author(s)

Organizer

Data Source

Saikawa Takafumi 才川隆文