Skip to Main content


Researcher identifiers

Number of documents


Érik Martin-Dorel's publications

Brought to you by HAL.

Journal articles3 documents

Conference papers8 documents

  • Guillaume Bertholon, Érik Martin-Dorel, Pierre Roux. Primitive Floats in Coq. ITP 2019, Interactive Theorem Proving, Sep 2019, PORTLAND, United States. ⟨10.4230/LIPIcs.ITP.2019.7⟩. ⟨hal-02449191⟩
  • Érik Martin-Dorel, Sergei Soloviev. Cumulative Effects in Learning. 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Mar 2018, Aussois, France. ⟨hal-02982569⟩
  • Érik Martin-Dorel, Pierre Roux. A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.90 - 99, ⟨10.1145/3018610.3018622⟩. ⟨hal-01510979⟩
  • Érik Martin-Dorel, Micaela Mayero, Ioana Pasca, Laurence Rideau, Laurent Théry. Certified, Efficient and Sharp Univariate Taylor Models in COQ. SYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania. ⟨hal-00845791v2⟩
  • Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, et al.. Rigorous Polynomial Approximation using Taylor Models in Coq. Fourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15. ⟨ensl-00653460v2⟩
  • Nicolas Brisebarre, Mioara Maria Joldes, Peter Kornerup, Érik Martin-Dorel, Jean-Michel Muller. Augmented precision square roots, 2-D norms, and discussion on correctly rounding {x^2+y^2}. 20th IEEE Symposium on Computer Arithmetic (ARITH-20), Jul 2011, Tübingen, Germany. pp.23-30, ⟨10.1109/ARITH.2011.13⟩. ⟨ensl-00545591v2⟩
  • Nicolas Brisebarre, Milos Ercegovac, Nicolas Louvet, Erik Martin-Dorel, Jean-Michel Muller, et al.. Implementing decimal floating-point arithmetic through binary: some suggestions. 21st IEEE International Conference on Application-specific Systems, Architectures and Processors (ASAP'2010), Jul 2010, Rennes, France. pp.317-320. ⟨ensl-00463353v2⟩
  • Érik Martin-Dorel. Formalization of Hensel's lemma in Coq. TYPES 2010: The 17th Workshop on Types for Proofs and Programs, Oct 2010, Warsaw, Poland. ⟨ensl-00560449⟩

Preprints, Working Papers, ...2 documents

  • Marc Daumas, David Lester, Erik Martin-Dorel, Annick Truffert. Stochastic Formal Methods for Hybrid Systems. 2009. ⟨hal-00107495v5⟩
  • Marc Daumas, Erik Martin-Dorel, Annick Truffert. Bornes quasi-certaines sur l'accumulation d'erreurs infimes dans les systèmes hybrides. 2008. ⟨hal-00333895⟩

Reports2 documents

  • Érik Martin-Dorel, Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Pay Functions. [Research Report] IRIT. 2017. ⟨hal-03109258⟩
  • Érik Martin-Dorel. Univariate and bivariate integral roots certificates based on Hensel's lifting. 2011. ⟨ensl-00575673⟩