| 2025 | FORTE | An Approach to Formalize Information-Theoretic Security of Multiparty Computation Protocols. | Cheng-Hui Weng, Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2025 | ITP | Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. | Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa |
| 2024 | ITP | Robust Mean Estimation by All Means (Short Paper). | Reynald Affeldt, Clark W. Barrett, Alessandro Bruni, Ieva Daukantas, Harun Khan, Takafumi Saikawa, Carsten Schrmann |
| 2024 | ITP | Typed Compositional Quantum Computation with Lenses. | Jacques Garrigue, Takafumi Saikawa |
| 2020 | ISITA | Formal Verification and Code-Generation of Mersenne-Twister Algorithm. | Takafumi Saikawa, Kazunari Tanaka, Kensaku Tanaka |
| 2019 | MPC | A Hierarchy of Monadic Effects for Program Verification Using Equational Reasoning. | Reynald Affeldt, David Nowak, Takafumi Saikawa |
| 2018 | ISITA | Examples of Formal Proofs about Data Compression. | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2016 | ISITA | Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |