| 2025 | APLAS | A Formal Foundation for Equational Reasoning on Probabilistic Programs. | Reynald Affeldt, Yoshihiro Ishiguro, Zachary Stone |
| 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 | Taming Differentiable Logics with Coq Formalisation. | Reynald Affeldt, Alessandro Bruni, Ekaterina Komendantskaya, Natalia Slusarz, Kathrin Stark |
| 2024 | ITP | A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq. | Reynald Affeldt, Zachary Stone |
| 2023 | APLAS | Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq. | Ayumu Saito, Reynald Affeldt |
| 2023 | CPP | Semantics of Probabilistic Programs using s-Finite Kernels in Coq. | Reynald Affeldt, Cyril Cohen, Ayumu Saito |
| 2022 | MPC | Towards a Practical Library for Monadic Equational Reasoning in Coq. | Ayumu Saito, Reynald Affeldt |
| 2020 | CADE | Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis. | Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Kazuhiko Sakaguchi |
| 2019 | ITP | Proving Tree Algorithms for Succinct Data Structures. | Reynald Affeldt, Jacques Garrigue, Xuanrui Qi, Kazunari 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 |
| 2017 | CPP | Formal foundations of 3D geometry to model robot manipulators. | Reynald Affeldt, Cyril Cohen |
| 2016 | ICFEM | Formal Verification of the rank Algorithm for Succinct Data Structures. | Akira Tanaka, Reynald Affeldt, Jacques Garrigue |
| 2016 | ISITA | Formalization of Reed-Solomon codes and progress report on formalization of LDPC codes. | Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa |
| 2015 | ITP | Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory. | Reynald Affeldt, Jacques Garrigue |
| 2014 | ISITA | Formalization of the variable-length source coding theorem: Direct part. | Ryosuke Obi, Manabu Hagiwara, Reynald Affeldt |
| 2012 | ITP | Formalization of Shannon's Theorems in SSReflect-Coq. | Reynald Affeldt, Manabu Hagiwara |
| 2012 | SAC | On construction of a library of formally verified low-level arithmetic functions. | Reynald Affeldt |
| 2007 | ProvSec | Formal Proof of Provable Security by Game-Playing in a Proof Assistant. | Reynald Affeldt, Miki Tanaka, Nicolas Marti |
| 2006 | ICFEM | Formal Verification of the Heap Manager of an Operating System Using Separation Logic. | Nicolas Marti, Reynald Affeldt, Akinori Yonezawa |
| 2002 | PEPM | Supporting objects in run-time bytecode specialization. | Reynald Affeldt, Hidehiko Masuhara, Eijiro Sumii, Akinori Yonezawa |