Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2016)

Examples of Formal Proofs about Data Compression. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (ISITA, 2018)

A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. - Reynald Affeldt; David Nowak; Takafumi Saikawa (MPC, 2019)

Formal Verification and Code-Generation of Mersenne-Twister Algorithm. - Takafumi Saikawa; Kazunari Tanaka; Kensaku Tanaka (ISITA, 2020)

Formal Adventures in Convex and Conical Spaces. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (CICM, 2020)

A Library for Formalization of Linear Error-Correcting Codes. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Autom. Reason., 2020)

A trustful monad for axiomatic reasoning with probability and nondeterminism. - Reynald Affeldt; Jacques Garrigue; David Nowak; Takafumi Saikawa (J. Funct. Program., 2021)

Robust Mean Estimation by All Means (Short Paper). - Reynald Affeldt; Clark W. Barrett; Alessandro Bruni; Ieva Daukantas; Harun Khan; Takafumi Saikawa; Carsten Schürmann (ITP, 2024)

Typed Compositional Quantum Computation with Lenses. - Jacques Garrigue; Takafumi Saikawa (ITP, 2024)

QECC: Quantum Computation and Error-Correcting Codes. - Jacques Garrigue; Takafumi Saikawa (DROPS Artifacts, 2024)

An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. - Cheng-Hui Weng; Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (FORTE, 2025)

A practical formalization of monadic equational reasoning in dependent-type theory. - Reynald Affeldt; Jacques Garrigue; Takafumi Saikawa (J. Funct. Program., 2025)