Updated on 2025/10/22

写真a

 
SAIKAWA Takafumi
 
Organization
Graduate School of Mathematics Division of Mathematics Designated Assistant Professor
Title
Designated Assistant Professor

Research Interests 9

  1. Coq

  2. Formal Verification

  3. Formalization

  4. Functional Programming

  5. Mathematical Logic

  6. OCaml

  7. Quantum Computing

  8. Rocq

  9. Type Theory

To the head of Research Interests.▲

Research Areas 3

  1. Informatics / Software  / Formal Verification of Programs, Functional Programming

  2. Informatics / Information theory  / Formalization of mathematics, Quantum Computation

  3. Natural Science / Basic mathematics  / Type Theory

To the head of Research Areas.▲

Research History 3

  1. Nagoya University   Graduate School of Mathematics   Designated Assistant Professor

    2025.4

    　 More details

    Country：Japan

  2. Nagoya University   Graduate School of Mathematics   Researcher

    2020.9 - 2025.3

    　 More details

    Country：Japan

  3. Peano System Inc.   Board member

    2016.11 - 2020.2

    　 More details

    Country：Japan

To the head of Research History.▲

Committee Memberships 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   

To the head of Committee Memberships.▲
 

Papers 15

  1. Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. Reviewed Open Access

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

    16th International Conference on Interactive Theorem Proving(ITP)     page： 21 - 20   2025.9

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2025.21

    Open Access

    Other Link： https://dblp.uni-trier.de/db/conf/itp/itp2025.html#AffeldtBC0S25

  2. A practical formalization of monadic equational reasoning in dependent-type theory. Reviewed Open Access

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Journal of Functional Programming   Vol. 35   2025.1

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1017/s0956796824000157

    Open Access

  3. Typed Compositional Quantum Computation with Lenses. Reviewed Open Access

    Jacques Garrigue, Takafumi Saikawa

    15th International Conference on Interactive Theorem Proving(ITP)     page： 15 - 18   2024.9

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2024.15

    Open Access

    Other Link： https://dblp.uni-trier.de/db/conf/itp/itp2024.html#GarrigueS24

  4. Robust Mean Estimation by All Means (Short Paper). Reviewed 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)     page： 39 - 8   2024.9

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Schloss Dagstuhl - Leibniz-Zentrum für Informatik  

    DOI： 10.4230/LIPIcs.ITP.2024.39

    Open Access

    Other Link： 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. Reviewed International journal Open Access

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

    Scientific reports   Vol. 14 ( 1 ) page： 12021 - 12021   2024.5

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    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. Reviewed Open Access

    Reynald Affeldt, Jacques Garrigue, David Nowak, Takafumi Saikawa

    Journal of Functional Programming   Vol. 31 - 17   2021.7

    　More details

    Authorship：Corresponding author   Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1017/S0956796821000137

  7. Formal Verification and Code-Generation of Mersenne-Twister Algorithm. Reviewed

    Takafumi Saikawa, Kazunari Tanaka, Kensaku Tanaka

    International Symposium on Information Theory and Its Applications(ISITA)     page： 607 - 611   2021.3

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

    Other Link： 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. Invited Reviewed International journal Open Access

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

    Scientific reports   Vol. 10 ( 1 ) page： 20740 - 20740   2020.11

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    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. Reviewed Open Access

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Intelligent Computer Mathematics - 13th International Conference(CICM)     page： 23 - 38   2020.7

    　More details

    Authorship：Corresponding author   Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer  

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

    Other Link： https://dblp.uni-trier.de/db/conf/mkm/cicm2020.html#AffeldtGS20

  10. Reasoning with Conditional Probabilities and Joint Distributions in Coq Reviewed Open Access

    AFFELDT Reynald, GARRIGUE Jacques, SAIKAWA Takafumi

    Computer Software   Vol. 37 ( 3 ) page： 3_79 - 3_95   2020.7

    　More details

    Language：English   Publishing type：Research paper (scientific journal)   Publisher：Japan Society for Software Science and Technology  

    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

    Other Link： 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

    　More details

    Language：English   Publishing type：Doctoral thesis  

  12. A Library for Formalization of Linear Error-Correcting Codes. Reviewed

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    Journal of Automated Reasoning   Vol. 64 ( 6 ) page： 1123 - 1164   2020.1

    　More details

    Language：English   Publishing type：Research paper (scientific journal)  

    DOI： 10.1007/s10817-019-09538-8

    Other Link： https://dblp.uni-trier.de/db/journals/jar/jar64.html#AffeldtGS20

  13. A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. Reviewed Open Access

    Reynald Affeldt, David Nowak, Takafumi Saikawa

    Mathematics of Program Construction - 13th International Conference(MPC)     page： 226 - 254   2019.10

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：Springer  

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

    Other Link： https://dblp.uni-trier.de/db/conf/mpc/mpc2019.html#AffeldtNS19

  14. Examples of Formal Proofs about Data Compression. Reviewed

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    International Symposium on Information Theory and Its Applications(ISITA)   Vol. 55   page： 633 - 637   2018.10

    　More details

    Language：English   Publisher：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

    Other Link： 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. Reviewed

    Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa

    2016 International Symposium on Information Theory and Its Applications(ISITA)     page： 532 - 536   2017.2

    　More details

    Language：English   Publishing type：Research paper (international conference proceedings)   Publisher：IEEE  

    Other Link： https://dblp.uni-trier.de/rec/conf/isita/2016

▼display all

To the head of Papers.▲

Books 1

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

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

    オーム社  2013.3  （ ISBN:9784274069116 ）

    　More details

To the head of Books.▲

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)     page： 182 - 192   2025

    　More details

  2. Auditing Disease Similarity Matrix Toward Automated Generation of Disease Maps

    HIRABAYASHI Soichiro, SAIKAWA Takafumi, HAYAKAWA Yoshihiko, OKUMURA Takashi

    JSAI Technical Report, SIG-KBS   Vol. 119   page： 07   2020.3

    　More details

    Language：Japanese   Publisher：The Japanese Society for Artificial Intelligence  

    DOI： 10.11517/jsaikbs.119.0_07

    CiNii Research

    Other Link： https://ndlsearch.ndl.go.jp/books/R000000004-I030292031

To the head of MISC.▲

Presentations 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 

    　More details

    Event date： 2024.9

    Language：English   Presentation type：Oral presentation (general)  

  2. Environment-friendly monadic equational reasoning for OCaml

    Reynald Affeld, Jacques Garrigue, Takafumi Saikawa

    The Coq Workshop 2023, Białystok, Poland  2023.7.31 

    　More details

    Event date： 2023.7

    Language：English   Presentation type：Oral presentation (general)  

  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 

    　More details

    Event date： 2022.6

    Language：English   Presentation type：Oral presentation (general)  

  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 

    　More details

    Event date： 2020.7

    Language：English   Presentation type：Oral presentation (general)  

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

    Takafumi Saikawa, Kazunori Matsuda, Yosuke Tsuji

    The Rocqshop 2025, Reykjavik, Iceland  2025.9.27 

    　More details

    Presentation type：Oral presentation (general)  

  6. A formalization of mathematical analysis in Rocq prover

    Takafumi Saikawa

    中央研究院資訊科學研究所 學術演講  2025.3.24 

    　More details

    Language：English   Presentation type：Public lecture, seminar, tutorial, course, or other speech  

▼display all

To the head of Presentations.▲

KAKENHI (Grants-in-Aid for Scientific Research) 5

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

    Grant number：25K03098  2025.4 - 2029.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (B)

  2. Application of Proof Assistants to the Exploration for Novel Mathematical Theorems

    Grant number：24K14820  2024.4 - 2027.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

  3. Formal Foundations for Verification of Physical and Probabilistic Systems

    Grant number：22H00520  2022.4 - 2026.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (A)

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

    Grant number：22K11902  2022.4 - 2025.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (C)

  5. Formalization on Modern Coding Theory

    Grant number：25289118  2013.4 - 2016.3

    Japan Society for the Promotion of Science  Grants-in-Aid for Scientific Research  Grant-in-Aid for Scientific Research (B)

    Hagiwara Manabu, Reynald Affeldt, KASAI Kenta, KUZUOKA Shigeaki, Garrigue Jacques, MIZOGUCHI Yoshihiro, NATION James B., OBI Ryosuke, NAKANO Kyosuke, SAIKAWA Takafumi

    　 More details

    To formalize modern coding theory, our research formalized "(spatially coupled) LDPC codes", "sum-product decoding algorithm" and related topics and also developed related theories. For example, we formalized channel capacities over BEC and BSEC, properties of stopping set, and Reed-Solomong codes and Euclidean decoding algorithm. We have organized workshops and open our result through web-sites.

To the head of KAKENHI (Grants-in-Aid for Scientific Research).▲