A hierarchy of monadic effects for program verification using equational reasoning R Affeldt, D Nowak, T Saikawa Mathematics of Program Construction: 13th International Conference, MPC 2019 …, 2019 | 27 | 2019 |
A trustful monad for axiomatic reasoning with probability and nondeterminism R Affeldt, J Garrigue, D Nowak, T Saikawa Journal of Functional Programming 31, e17, 2021 | 9 | 2021 |
Reasoning with conditional probabilities and joint distributions in Coq R Affeldt, J Garrigue, T Saikawa コンピュータ ソフトウェア 37 (3), 3_79-3_95, 2020 | 9 | 2020 |
Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes R Affeldt, J Garrigue, T Saikawa 2016 International Symposium on Information Theory and Its Applications …, 2016 | 9 | 2016 |
A library for formalization of linear error-correcting codes R Affeldt, J Garrigue, T Saikawa Journal of Automated Reasoning 64 (6), 1123-1164, 2020 | 8 | 2020 |
Examples of formal proofs about data compression R Affeldt, J Garrigue, T Saikawa 2018 International Symposium on Information Theory and Its Applications …, 2018 | 5 | 2018 |
A Coq formalization of information theory and linear error-correcting codes R Affeldt, M Hagiwara, J Sénizergues, J Garrigue, K Sakaguchi, T Asai, ... | 5 | 2018 |
Formal Verification and Code-Generation of Mersenne-Twister Algorithm T Saikawa, K Tanaka, K Tanaka 2020 International Symposium on Information Theory and Its Applications …, 2020 | 4 | 2020 |
Monadic equational reasoning in Coq R Affeldt, J Garrigue, D Nowak, T Saikawa, C Sauvage, K Tanaka | 4 | 2019 |
Validating OCaml soundness by translation into Coq J Garrigue, T Saikawa Proc. 28th International Conference on Types for Proofs and Programs, 2022 | 3 | 2022 |
Strategies for the efficient use of diagnostic resource under constraints: a model-based study on overflow of patients and insufficient diagnostic kits N Tsuchida, F Nakamura, K Matsuda, T Saikawa, T Okumura Scientific Reports 10 (1), 20740, 2020 | 3 | 2020 |
Environment-friendly monadic equational reasoning for OCaml R Affeldt, J Garrigue, T Saikawa The Coq Workshop, 2023 | 1 | 2023 |
Formal adventures in convex and conical spaces R Affeldt, J Garrigue, T Saikawa International Conference on Intelligent Computer Mathematics, 23-38, 2020 | 1 | 2020 |
A Practical Formalization of Monadic Equational Reasoning in Dependent-type Theory R Affeldt, J Garrigue, T Saikawa arXiv preprint arXiv:2312.06103, 2023 | | 2023 |
Typed compositional quantum computation with lenses J Garrigue, T Saikawa arXiv preprint arXiv:2311.14347, 2023 | | 2023 |
A type-theoretic account of quantum computation JGT Saikawa | | 2023 |
Formalization of Equational Reasoning in the Set-Theoretic Interpretation of Type Theory T Saikawa (No Title), 2020 | | 2020 |
Auditing Disease Similarity Matrix Toward Automated Generation of Disease Maps S HIRABAYASHI, T SAIKAWA, Y HAYAKAWA, T OKUMURA 人工知能学会知識ベースシステム研究会資料 119, 35-40, 2020 | | 2020 |
Examples of Formal Proofs about Data Compression A Reynald, G Jacques, S Takafumi IEICE Proceeding Series, 665-669, 2018 | | 2018 |
Interpreting OCaml GADTs into Coq J Garrigue, T Saikawa | | |