A Formal Theory of Cooperative TU-Games. - Marc Daumas; Érik Martin-Dorel; Annick Truffert; Michel Ventou (MDAI, 2009)

Stochastic Formal Methods for Hybrid Systems. - Marc Daumas; Érik Martin-Dorel; David R. Lester; Annick Truffert (NASA Formal Methods, 2009)

Implementing decimal floating-point arithmetic through binary: Some suggestions. - Nicolas Brisebarre; Nicolas Louvet; Érik Martin-Dorel; Jean-Michel Muller; Adrien Panhaleux; Milos D. Ercegovac (ASAP, 2010)

Improved bound for stochastic formal correctness of numerical algorithms. - Marc Daumas; David R. Lester; Érik Martin-Dorel; Annick Truffert (Innov. Syst. Softw. Eng., 2010)

Augmented Precision Square Roots and 2-D Norms, and Discussion on Correctly Rounding sqrt(x^2+y^2). - Nicolas Brisebarre; Mioara Joldes; Peter Kornerup; Érik Martin-Dorel; Jean-Michel Muller (IEEE Symposium on Computer Arithmetic, 2011)

Rigorous Polynomial Approximation Using Taylor Models in Coq. - Nicolas Brisebarre; Mioara Joldes; Érik Martin-Dorel; Micaela Mayero; Jean-Michel Muller; Ioana Pasca; Laurence Rideau; Laurent Théry (NASA Formal Methods, 2012)

Contributions to the Formal Verification of Arithmetic Algorithms. (Contributions à la vérification formelle d'algorithmes arithmétiques). - Érik Martin-Dorel (2012)

Certified, Efficient and Sharp Univariate Taylor Models in COQ. - Érik Martin-Dorel; Laurence Rideau; Laurent Théry; Micaela Mayero; Ioana Pasca (SYNASC, 2013)

Formally Verified Certificate Checkers for Hardest-to-Round Computation. - Érik Martin-Dorel; Guillaume Hanrot; Micaela Mayero; Laurent Théry (J. Autom. Reason., 2015)

A Formal Study of Boolean Games with Random Formulas as Payoff Functions. - Érik Martin-Dorel; Sergei Soloviev (TYPES, 2016)

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. - Érik Martin-Dorel; Guillaume Melquiond (J. Autom. Reason., 2016)

A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. - Érik Martin-Dorel; Pierre Roux 001 (CPP, 2017)

An Existence Theorem of Nash Equilibrium in Coq and Isabelle. - Stéphane Le Roux 001; Érik Martin-Dorel; Jan-Georg Smaus (GandALF, 2017)

Primitive Floats in Coq. - Guillaume Bertholon; Érik Martin-Dorel; Pierre Roux 001 (ITP, 2019)

Games of incomplete information: A framework based on belief functions. - Pierre Pomeret-Coquot; Hélène Fargier; Érik Martin-Dorel (Int. J. Approx. Reason., 2022)

Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant. - Pierre Pomeret-Coquot; Hélène Fargier; Érik Martin-Dorel (ITP, 2023)

Enabling Floating-Point Arithmetic in the Coq Proof Assistant. - Érik Martin-Dorel; Guillaume Melquiond; Pierre Roux 001 (J. Autom. Reason., 2023)

Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users. - Ana de Almeida Borges; Annalí Casanueva Artís; Jean-Rémy Falleri; Emilio Jesús Gallego Arias; Érik Martin-Dorel; Karl Palmskog; Alexander Serebrenik; Théo Zimmermann (J. Autom. Reason., 2025)