Takafumi Saikawa

J. Funct. Program., 2025

2024

QECC: Quantum Computation and Error-Correcting Codes.

[BibT_eX]

[DOI]

Dataset, November, 2024

Typed Compositional Quantum Computation with Lenses.

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Robust Mean Estimation by All Means (Short Paper).

[BibT_eX]

[DOI]

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2021

A trustful monad for axiomatic reasoning with probability and nondeterminism.

[BibT_eX]

[DOI]

J. Funct. Program., 2021

2020

A Library for Formalization of Linear Error-Correcting Codes.

[BibT_eX]

[DOI]

J. Autom. Reason., 2020

Formal Adventures in Convex and Conical Spaces.

[BibT_eX]

[DOI]

Proceedings of the Intelligent Computer Mathematics - 13th International Conference, 2020

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

[BibT_eX]

[DOI]

Kazunari Tanaka

Kensaku Tanaka

Proceedings of the International Symposium on Information Theory and Its Applications, 2020

2019

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning.

[BibT_eX]

[DOI]

David Nowak

Proceedings of the Mathematics of Program Construction - 13th International Conference, 2019

2018

Examples of Formal Proofs about Data Compression.

[BibT_eX]

[DOI]

Proceedings of the International Symposium on Information Theory and Its Applications, 2018

2016

Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes.

[BibT_eX]

[DOI]