| 2025 | ITP | Formalizing Concentration Inequalities in Rocq: Infrastructure and Automation. | Reynald Affeldt, Alessandro Bruni, Cyril Cohen, Pierre Roux, Takafumi Saikawa |
| 2024 | ESOP | Trocq: Proof Transfer for Free, With or Without Univalence. | Cyril Cohen, Enzo Crance, Assia Mahboubi |
| 2024 | ESOP | Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. | Cyril Cohen, Enzo Crance, Assia Mahboubi |
| 2023 | CPP | Semantics of Probabilistic Programs using s-Finite Kernels in Coq. | Reynald Affeldt, Cyril Cohen, Ayumu Saito |
| 2021 | ITP | Unsolvability of the Quintic Formalized in Dependent Type Theory. | Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
| 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 |
| 2020 | FSCD | Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). | Cyril Cohen, Kazuhiko Sakaguchi, Enrico Tassi |
| 2019 | ITP | Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. | Ran Chen, Cyril Cohen, Jean-Jacques Lvy, Stephan Merz, Laurent Thry |
| 2018 | ITP | Towards Certified Meta-Programming with Typed Template-Coq. | Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, Nicolas Tabareau |
| 2017 | CPP | Formal foundations of 3D geometry to model robot manipulators. | Reynald Affeldt, Cyril Cohen |
| 2017 | ITP | A Formal Proof in Coq of LaSalle's Invariance Principle. | Cyril Cohen, Damien Rouhling |
| 2016 | CPP | Formalization of a newton series representation of polynomials. | Cyril Cohen, Boris Djalal |
| 2014 | ITP | A Coq Formalization of Finitely Presented Modules. | Cyril Cohen, Anders Mrtberg |
| 2013 | CPP | Refinements for Free! | Cyril Cohen, Maxime Dns, Anders Mrtberg |
| 2013 | ITP | Pragmatic Quotient Types in Coq. | Cyril Cohen |
| 2013 | ITP | A Machine-Checked Proof of the Odd Order Theorem. | Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, Franois Garillot, Stphane Le Roux, Assia Mahboubi, Russell O'Connor, Sidi Ould Biha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, Laurent Thry |
| 2012 | ITP | Construction of Real Algebraic Numbers in Coq. | Cyril Cohen |
| 2010 | AISC | A Formal Quantifier Elimination for Algebraically Closed Fields. | Cyril Cohen, Assia Mahboubi |