2025/10/22 更新

写真a

サイカワ　タカフミ
才川　隆文
SAIKAWA Takafumi
所属
大学院多元数理科学研究科 多元数理科学専攻 特任助教
職名
特任助教

研究キーワード 9

  1. Coq

  2. Formal Verification

  3. Formalization

  4. Functional Programming

  5. Mathematical Logic

  6. OCaml

  7. Quantum Computing

  8. Rocq

  9. Type Theory

研究キーワードの先頭へ▲

研究分野 3

  1. 情報通信 / ソフトウェア  / Formal Verification of Programs, Functional Programming

  2. 情報通信 / 情報学基礎論  / Formalization of mathematics, Quantum Computation

  3. 自然科学一般 / 数学基礎  / Type Theory

研究分野の先頭へ▲

経歴 3

  1. 名古屋大学   大学院多元数理科学研究科   特任助教

    2025年4月 - 現在

    　 詳細を見る

    国名：日本国

  2. 名古屋大学   大学院多元数理科学研究科   研究員

    2020年9月 - 2025年3月

    　 詳細を見る

    国名：日本国

  3. 株式会社ぺあのしすてむ   取締役

    2016年11月 - 2020年2月

    　 詳細を見る

    国名：日本国

経歴の先頭へ▲

委員歴 3

  1. OCaml Users and Developers Workshop 2024 (Milan, Italy)   Program committee member  

    2024年   

  2. OCaml Users and Developers Workshop 2022 (Ljubljana, Slovenia)   Program committee member  

    2022年   

  3. The 17th Theorem Proving and Provers meeting (TPP 2021)   Organizer  

    2021年   

委員歴の先頭へ▲
 

論文 15

  1. Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. 査読有り Open Access

    Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa

    16th International Conference on Interactive Theorem Proving(ITP)     頁： 21 - 20   2025年9月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2025.21

    Open Access

    その他リンク： https://dblp.uni-trier.de/db/conf/itp/itp2025.html#AffeldtBC0S25

  2. A practical formalization of monadic equational reasoning in dependent-type theory. 査読有り Open Access

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Journal of Functional Programming   35 巻   2025年1月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1017/s0956796824000157

    Open Access

  3. Typed Compositional Quantum Computation with Lenses. 査読有り Open Access

    Jacques Garrigue, Takafumi Saikawa

    15th International Conference on Interactive Theorem Proving(ITP)     頁： 15 - 18   2024年9月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2024.15

    Open Access

    その他リンク： https://dblp.uni-trier.de/db/conf/itp/itp2024.html#GarrigueS24

  4. Robust Mean Estimation by All Means (Short Paper). 査読有り Open Access

    Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schürmann

    15th International Conference on Interactive Theorem Proving(ITP)     頁： 39 - 8   2024年9月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2024.39

    Open Access

    その他リンク： https://dblp.uni-trier.de/db/conf/itp/itp2024.html#AffeldtBBDKSS24

  5. Linear regression model for metal-organic frameworks with CO2 adsorption based on topological data analysis. 査読有り 国際誌 Open Access

    Kazuto Akagi, Hisashi Naito, Takafumi Saikawa, Motoko Kotani, Hirofumi Yoshikawa

    Scientific reports   14 巻 ( 1 ) 頁： 12021 - 12021   2024年5月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    Metal-organic frameworks (MOFs), self-assembled porous materials synthesized from metal ions and organic ligands, are promising candidates for the direct capture of CO2 from the atmosphere. In this work, we developed a regression model to predict the optimal component of the MOF that governs the amount of CO2 adsorption per volume based on experimentally observed adsorption and structure data combined with MOF adsorption sites. The structural descriptors were generated by topological data analysis with persistence diagrams, an advanced mathematical method for quantifying the rings and cavities within the MOF. This enables us to analyze direct effects and significance of the geometric structure of the MOF on the efficiency of CO2 adsorption in a novel way. The proposed approach is proved to be highly correlated with experimental data and thus offers an effective screening tool for MOFs with optimized structures.

    DOI： 10.1038/s41598-024-62858-7

    Open Access

    PubMed

  6. A trustful monad for axiomatic reasoning with probability and nondeterminism. 査読有り Open Access

    Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

    Journal of Functional Programming   31 巻 - 17   2021年7月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1017/S0956796821000137

  7. Formal Verification and Code-Generation of Mersenne-Twister Algorithm. 査読有り

    Takafumi Saikawa, Kazunari Tanaka, Kensaku Tanaka

    International Symposium on Information Theory and Its Applications(ISITA)     頁： 607 - 611   2021年3月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IEEE  

    その他リンク： https://dblp.uni-trier.de/rec/conf/isita/2020

  8. Strategies for the efficient use of diagnostic resource under constraints: a model-based study on overflow of patients and insufficient diagnostic kits. 招待有り 査読有り 国際誌 Open Access

    Naoshi Tsuchida, Fumihiko Nakamura, Kazunori Matsuda, Takafumi Saikawa, Takashi Okumura

    Scientific reports   10 巻 ( 1 ) 頁： 20740 - 20740   2020年11月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    This article addresses an optimisation problem of distributing rapid diagnostic kits among patients when the demands far surpass the supplies. This problem has not been given much attention in the field, and therefore, this article aims to provide a preliminary result in this problem domain. First, we describe the problem and define the goal of the optimisation by introducing an evaluation metric that measures the efficiency of the distribution strategies. Then, we propose two simple strategies, and a strategy that incorporates a prediction of patients' visits utilising a standard epidemic model. The strategies were evaluated using the metric, with past statistics in Kitami City, Hokkaido, Japan, and the prediction-based strategy outperformed the other distribution strategies. We discuss the properties of the strategies and the limitations of the proposed approach. Although the problem must be generalised before the actual deployment of the suggested strategy, the preliminary result is promising in its ability to address the shortage of diagnostic capacity currently observed worldwide because of the ongoing coronavirus disease pandemic.

    DOI： 10.1038/s41598-020-77468-2

    Open Access

    PubMed

  9. Formal Adventures in Convex and Conical Spaces. 査読有り Open Access

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Intelligent Computer Mathematics - 13th International Conference(CICM)     頁： 23 - 38   2020年7月

    　詳細を見る

    担当区分：責任著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer  

    DOI： 10.1007/978-3-030-53518-6_2

    その他リンク： https://dblp.uni-trier.de/db/conf/mkm/cicm2020.html#AffeldtGS20

  10. Reasoning with Conditional Probabilities and Joint Distributions in Coq 査読有り Open Access

    AFFELDT Reynald, GARRIGUE Jacques, SAIKAWA Takafumi

    コンピュータ ソフトウェア   37 巻 ( 3 ) 頁： 3_79 - 3_95   2020年7月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：日本ソフトウェア科学会  

    Probabilities occur in many applications of computer science, such as communication theory and artificial intelligence. These are critical applications that require some form of verification to guarantee the quality of their implementations. Unfortunately, probabilities are also the typical example of a mathematical theory whose abuses of notations make pencil-and-paper proofs difficult to formalize. In this paper, we experiment a new formalization of conditional probabilities that we validate with two applications. First, we formalize the foundational definitions and theorems of information theory, extending previous work with new lemmas. Second, we formalize the notion of conditional independence and its properties, paving the road for a formalization of probabilistic graphical models.

    DOI： 10.11309/jssst.37.3_79

    Open Access

    CiNii Research

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030585163

  11. Formalization of Equational Reasoning in the Set-Theoretic Interpretation of Type Theory

    Takafumi Saikawa

        2020年5月

    　詳細を見る

    記述言語：英語   掲載種別：学位論文（博士）  

  12. A Library for Formalization of Linear Error-Correcting Codes. 査読有り

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Journal of Automated Reasoning   64 巻 ( 6 ) 頁： 1123 - 1164   2020年1月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（学術雑誌）  

    DOI： 10.1007/s10817-019-09538-8

    その他リンク： https://dblp.uni-trier.de/db/journals/jar/jar64.html#AffeldtGS20

  13. A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. 査読有り Open Access

    Reynald Affeldt, David Nowak, Takafumi Saikawa

    Mathematics of Program Construction - 13th International Conference(MPC)     頁： 226 - 254   2019年10月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer  

    DOI： 10.1007/978-3-030-33636-3_9

    その他リンク： https://dblp.uni-trier.de/db/conf/mpc/mpc2019.html#AffeldtNS19

  14. Examples of Formal Proofs about Data Compression. 査読有り

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    International Symposium on Information Theory and Its Applications(ISITA)   55 巻   頁： 633 - 637   2018年10月

    　詳細を見る

    記述言語：英語   出版者・発行元：IEEE  

    Because of the increasing complexity of mathematical proofs, there is a growing interest in formalization using proof-assistants. In this paper, we explain new formal proofs of standard lemmas in data compression (Jensen’s and Kraft’s inequalities) as well as concrete applications (to the analysis of compression methods and Shannon-Fano codes). We explain in particular how one turns the paper proof into formal terms and the relation between the informal proof and the formal one. These formalizations come as an extension to an existing formal library for information theory and error-correcting codes.

    DOI： 10.23919/ISITA.2018.8664276

    CiNii Research

    その他リンク： https://dblp.uni-trier.de/db/conf/isita/isita2018.html#AffeldtGS18

  15. Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. 査読有り

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    2016 International Symposium on Information Theory and Its Applications(ISITA)     頁： 532 - 536   2017年2月

    　詳細を見る

    記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：IEEE  

    その他リンク： https://dblp.uni-trier.de/rec/conf/isita/2016

▼全件表示

論文の先頭へ▲

書籍等出版物 1

  1. 型システム入門 : プログラミング言語と型の理論

    Pierce, Benjamin C., 住井 英二郎, 遠藤 侑介, 酒井 政裕, 今井 敬吾, 黒木 裕介, 今井 宜洋, 才川 隆文, 今井 健男

    オーム社  2013年3月  （ ISBN:9784274069116 ）

    　詳細を見る

    総ページ数：xxi, 503p   記述言語：日本語

    CiNii Research

    その他リンク： https://search.ebscohost.com/login.aspx?direct=true&db=edsebk&AN=712433&site=ehost-live

書籍等出版物の先頭へ▲

MISC 2

  1. An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols.

    Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa  

    Formal Techniques for Distributed Objects, Components, and Systems - 45th IFIP WG 6.1 International Conference(FORTE)   頁： 182 - 192   2025年

    　詳細を見る

    出版者・発行元：Springer  

    DOI： 10.1007/978-3-031-95497-9_11

    その他リンク： https://dblp.uni-trier.de/db/conf/forte/forte2025.html#WengAGS25

  2. 疾患類似度の距離マトリックス生成に向けた監査手法の提案

    平林 宗一郎, 才川 隆文, 早川 吉彦, 奥村 貴史  

    人工知能学会研究会資料 知識ベースシステム研究会119 巻   頁： 07   2020年3月

    　詳細を見る

    記述言語：日本語   出版者・発行元：一般社団法人 人工知能学会  

    DOI： 10.11517/jsaikbs.119.0_07

    CiNii Research

    その他リンク： https://ndlsearch.ndl.go.jp/books/R000000004-I030292031

MISCの先頭へ▲

講演・口頭発表等 6

  1. Typed compositional quantum computation with lenses

    Jacques Garrigue, Takafumi Saikawa

    The 15th International Conference on Interactive Theorem Proving (ITP 2024), Tbilisi, Georgia  2024年9月10日 

    　詳細を見る

    開催年月日： 2024年9月

    記述言語：英語   会議種別：口頭発表（一般）  

  2. Environment-friendly monadic equational reasoning for OCaml

    Reynald Affeld, Jacques Garrigue, Takafumi Saikawa

    The Coq Workshop 2023, Białystok, Poland  2023年7月31日 

    　詳細を見る

    開催年月日： 2023年7月

    記述言語：英語   会議種別：口頭発表（一般）  

  3. Validating OCaml soundness by translation into Coq

    Jacques Garrigue, Takafumi Saikawa

    The 28th International Conference on Types for Proofs and Programs (TYPES 2022), Nantes, France  2022年6月23日 

    　詳細を見る

    開催年月日： 2022年6月

    記述言語：英語   会議種別：口頭発表（一般）  

  4. Formal adventures in convex and conical spaces

    Reynald Affeld, Jacques Garrigue, Takafumi Saikawa

    The 13th Conference on Intelligent Computer Mathematics (CICM 2020)  2020年7月27日 

    　詳細を見る

    開催年月日： 2020年7月

    記述言語：英語   会議種別：口頭発表（一般）  

  5. Formalization of matching numbers with finmap and mathcomp-classical

    Takafumi Saikawa, Kazunori Matsuda, Yosuke Tsuji

    The Rocqshop 2025, Reykjavik, Iceland  2025年9月27日 

    　詳細を見る

    会議種別：口頭発表（一般）  

  6. A formalization of mathematical analysis in Rocq prover

    Takafumi Saikawa

    中央研究院資訊科學研究所 學術演講  2025年3月24日 

    　詳細を見る

    記述言語：英語   会議種別：公開講演，セミナー，チュートリアル，講習，講義等  

▼全件表示

講演・口頭発表等の先頭へ▲

科研費 5

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

    研究課題/研究課題番号：25K03098  2025年4月 - 2029年3月

    日本学術振興会  科学研究費助成事業  基盤研究(B)

    J Garrigue, 才川 隆文, Affeldt Reynald, 田中 哲, 勝股 審也

  2. 定理証明支援系を用いた数学的定理の発見的証明

    研究課題/研究課題番号：24K14820  2024年4月 - 2027年3月

    日本学術振興会  科学研究費助成事業  基盤研究(C)

    才川 隆文, 松田 一徳

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

    研究課題/研究課題番号：22H00520  2022年4月 - 2026年3月

    日本学術振興会  科学研究費助成事業  基盤研究(A)

    Affeldt Reynald, J Garrigue, 勝股 審也, 溝口 佳寛, 中野 圭介, 才川 隆文

    　 詳細を見る

    本プロジェクトの目的は、外界の物理的対象と直接対話し動作するプログラムの品質評価のため、定理証明支援系上の検証基盤の設計に必要な検証技術の研究を行うことである。
    <BR>
    令和５年度、数学（とくに、確率論）と確率的プログラミング言語の形式化に集中した。数学の形式化に関して、MathComp-Analysisライブラリによる微分と積分の形式化を進展させ、新たな定理（ロピタルの定理、微分積分学の基本定理、カーネルに基づいたGiryモナドなど）で拡張し、ドキュメンテーションツールを開発した。その拡張は人工知能で使われている損失関数の性質を記述するための論理の形式化に応用した。確率論の形式化に関して、基本的な分布（ベルヌーイ、二項、連続一様など）の形式化を行った。Infotheoという情報理論のライブラリの有限確率の基盤の移植と拡張を行った。その拡張をロバスト統計に応用した（コペンハーゲンIT大学と共同研究）。
    <BR>
    等式推論技術に関して、Monaeというプログラム検証基盤をOCamlプログラミング言語の検証ができるように拡張した。量子計算に関して、モナドの構築にまだ至っていないものの、MathCompの上でShor符号を含むいくつか量子回路を形式化し、その正しさを証明できた。確率的プログラミング言語に関して、令和４年度形式化した一階確率的プログラミング言語の意味論を、依存型に基づく構文の形式化で拡張した。その拡張を用いて、等式推論によるプログラム検証の応用例を増やし、連続確率分布を考慮した等式推論の実現ができた。

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

    研究課題/研究課題番号：22K11902  2022年4月 - 2025年3月

    日本学術振興会  科学研究費助成事業  基盤研究(C)

    J Garrigue, 才川 隆文, Affeldt Reynald

    　 詳細を見る

    本年度は主にCoqに翻訳されたプログラムの証明方法について研究を行った．証明にはモナド等式理論に基いたMonaeというCoqのプログラム証明ライブラリを使っている．具体的にはプログラミング言語の様々な機能を圏論的なモナドとして表現し，その等式理論によってプログラムを証明する．昨年度は既にCoqgen (我々が開発したOCamlからCoqへのコンパイラとライブラリ) で実装された参照型を扱うモナドを直接にMonaeに埋め込むことで，MonaeによるCoqgenで翻訳されたプログラムの証明を実験的に行った．しかし，翻訳の完全性のためにCoqgenの実装はCoqの論理と矛盾する定義を可能にしており，昨年の翻訳方法ではMonaeの無矛盾性を保証することができなかった．本年度は問題を検証した上で実装を整理し，Coqの制限を解除しない，無矛盾な実装を用意した．また，OCamlから翻訳されたプログラム例を増やし，プログラムの証明に必要な公理(等式)を再構成した．参照型(ポインタ)を含むプログラムについて，通常は分離論理でしか証明できないと認識されているようなプログラムも扱えることを確認した．その結果をCoq Workshop 2023 (ビャウィストク開催) ， TPP 2023 (東京工業大学開催) および APLAS NIER 2023 (台北開催) で発表し，論文「A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory」の一部としてまとめた．

  5. モダン符号の形式化

    研究課題/研究課題番号：25289118  2013年4月 - 2016年3月

    日本学術振興会  科学研究費助成事業  基盤研究(B)

    萩原 学, AFFELDT Reynald, 笠井 健太, 葛岡 成晃, J Garrigue, 溝口 佳寛, 小尾 良介, 中野 恭輔, 才川 隆文

    　 詳細を見る

    モダン符号の形式化研究として、LDPC符号やsum-product復号に関する定義や性質の形式化や理論の発展を行った。必要に応じ、関連する話題の形式化にも着手した。具体的には、誤り訂正の限界に関わる二元消失通信路やその拡張である二元対称消失通信路の通信路容量の形式化、Stopping Setに関する形式化、実装時にLDPC符号と組合せて用いられることの多いReed-Solomon符号の形式化などである。本研究では、研究成果の普及活動として、ホームページによる成果公開や、ワークショップの開催も行った。

科研費の先頭へ▲