A Formal Quantifier Elimination for Algebraically Closed Fields. - Cyril Cohen; Assia Mahboubi (AISC/MKM/Calculemus, 2010)

Construction of Real Algebraic Numbers in Coq. - Cyril Cohen (ITP, 2012)

Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination - Cyril Cohen; Assia Mahboubi (Log. Methods Comput. Sci., 2012)

Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre). - Cyril Cohen (2012)

Refinements for Free! - Cyril Cohen; Maxime Dénès; Anders Mörtberg (CPP, 2013)

Pragmatic Quotient Types in Coq. - Cyril Cohen (ITP, 2013)

A Machine-Checked Proof of the Odd Order Theorem. - Georges Gonthier; Andrea Asperti; Jeremy Avigad; Yves Bertot; Cyril Cohen; François Garillot; Stéphane Le Roux 001; Assia Mahboubi; Russell O'Connor; Sidi Ould Biha; Ioana Pasca; Laurence Rideau; et al. (ITP, 2013)

A Coq Formalization of Finitely Presented Modules. - Cyril Cohen; Anders Mörtberg (ITP, 2014)

Formalization of a newton series representation of polynomials. - Cyril Cohen; Boris Djalal (CPP, 2016)

Formalized linear algebra over Elementary Divisor Rings in Coq. - Guillaume Cano; Cyril Cohen; Maxime Dénès; Anders Mörtberg; Vincent Siles (Log. Methods Comput. Sci., 2016)

Formal foundations of 3D geometry to model robot manipulators. - Reynald Affeldt; Cyril Cohen (CPP, 2017)

A Formal Proof in Coq of LaSalle's Invariance Principle. - Cyril Cohen; Damien Rouhling (ITP, 2017)

Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. - Cyril Cohen; Thierry Coquand; Simon Huber; Anders Mörtberg (FLAP, 2017)

Towards Certified Meta-Programming with Typed Template-Coq. - Abhishek Anand; Simon Boulier; Cyril Cohen; Matthieu Sozeau; Nicolas Tabareau (ITP, 2018)

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (CoRR, 2018)

Formalization Techniques for Asymptotic Reasoning in Classical Analysis. - Reynald Affeldt; Cyril Cohen; Damien Rouhling (J. Formaliz. Reason., 2018)

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle. - Ran Chen; Cyril Cohen; Jean-Jacques Lévy; Stephan Merz; Laurent Théry (ITP, 2019)

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 (IJCAR (2), 2020)

Hierarchy Builder: Algebraic hierarchies Made Easy in Coq with Elpi (System Description). - Cyril Cohen; Kazuhiko Sakaguchi; Enrico Tassi (FSCD, 2020)

The MetaCoq Project. - Matthieu Sozeau; Abhishek Anand; Simon Boulier; Cyril Cohen; Yannick Forster 002; Fabian Kunze; Gregory Malecha; Nicolas Tabareau; Théo Winterhalter (J. Autom. Reason., 2020)

Unsolvability of the Quintic Formalized in Dependent Type Theory. - Sophie Bernard; Cyril Cohen; Assia Mahboubi; Pierre-Yves Strub (ITP, 2021)

Semantics of Probabilistic Programs using s-Finite Kernels in Coq. - Reynald Affeldt; Cyril Cohen; Ayumu Saito (CPP, 2023)

Measure Construction by Extension in Dependent Type Theory with Application to Integration. - Reynald Affeldt; Cyril Cohen (J. Autom. Reason., 2023)

Trocq: Proof Transfer for Free, With or Without Univalence. - Cyril Cohen; Enzo Crance; Assia Mahboubi (ESOP (1), 2024)

Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. - Cyril Cohen; Enzo Crance; Assia Mahboubi (ESOP (1), 2024)

A bargain for mergesorts (functional pearl) - How to prove your mergesort correct and stable, almost for free. - Cyril Cohen; Kazuhiko Sakaguchi (CoRR, 2024)