Publications

Martin-Dorel, Erik

Pour une recherche plus ciblée, utiliser l'interface d'interrogation de la base des publications de l'IRIT.
For an advanced search, please use the IRIT's publications database form.

 

Articles de revues internationales / International journal papers

• Erik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Dans : Journal of Automated Reasoning, Springer-Verlag, Vol. 57 N. 3, p. 187-217, octobre 2016.
  Résumé Accès : http://dx.doi.org/10.1007/s10817-015-9350-4 - https://www.irit.fr/publis/ACADIE/CoqInterval-JAR.pdf - http://oatao.univ-toulouse.fr/16862/
  BibTeX

• Erik Martin-Dorel, Guillaume Hanrot, Micaela Mayero, Laurent Théry. Formally verified certificate checkers for hardest-to-round computation. Dans : Journal of Automated Reasoning, Springer-Verlag, Vol. 54 N. 1, p. 1-29, janvier 2015.
  Accès : http://dx.doi.org/10.1007/s10817-014-9312-2
  BibTeX

• Erik Martin-Dorel, Guillaume Melquiond, Jean-Michel Muller. Some issues related to double rounding. Dans : BIT Numerical Mathematics, Springer, Vol. 53 N. 4, p. 897-924, 2013.
  Accès : http://dx.doi.org/10.1007/s10543-013-0436-2
  BibTeX

• Marc Daumas, David Lester, Erik Martin-Dorel, Annick Truffert. Improved bound for stochastic formal correctness of numerical algorithms. Dans : Innovations in Systems and Software Engineering, Springer, Vol. 6 N. 3, p. 173-179, 2010.
  Accès : http://dx.doi.org/10.1007/s11334-010-0128-x
  BibTeX

Conférences et workshops internationaux / International conference papers

• Erik Martin-Dorel, Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Payoff Functions (regular paper). Dans : Types, Novi Sad, 23/05/16-26/05/16, Silvia Ghilezan, Herman Geuvers, Jelena Ivetic (Eds.), Schloss Dagstuhl Leibniz-Zentrum fur Informatik, LIPIcs Vol. 97, art. 14, p. 1-22, 2018.
  Résumé Accès : https://doi.org/10.4230/LIPIcs.TYPES.2016.14
  BibTeX

• Stéphane Le Roux, Erik Martin-Dorel, Jan-Georg Smaus. An Existence Theorem of Nash Equilibrium in Coq and Isabelle (regular paper). Dans : International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2017), Rome, Italie, 20/09/17-22/09/17, Vol. 256, Electronic Proceedings in Theoretical Computer Science (EPTCS), p. 46-60, septembre 2017.
  Accès : http://dx.doi.org/10.4204/EPTCS.256.4 - http://oatao.univ-toulouse.fr/19172/
  BibTeX

• Erik Martin-Dorel, Pierre Roux. A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations (regular paper). Dans : ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Paris, 16/01/17-17/01/17, ACM : Association for Computing Machinery, p. 90-99, janvier 2017.
  Accès : https://dx.doi.org/10.1145/3018610.3018622 - https://hal.archives-ouvertes.fr/hal-01510979 - http://oatao.univ-toulouse.fr/18859/
  BibTeX

• Erik Martin-Dorel, Micaela Mayero, Ioana Pasca, Laurence Rideau, Laurent Théry. Certified, Efficient and Sharp Univariate Taylor Models in COQ (regular paper). Dans : International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2013), Timisoara, Romania, 23/09/13-26/09/13, IEEE : Institute of Electrical and Electronics Engineers, p. 193-200, 2013.
  Accès : http://dx.doi.org/10.1109/SYNASC.2013.33
  BibTeX

• Nicolas Brisebarre, Mioara Joldes, Erik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry. Rigorous Polynomial Approximation Using Taylor Models in Coq (regular paper). Dans : International Symposium on NASA Formal Methods (NFM 2012), Norfolk, Virginia, 03/04/12-05/04/12, Springer, p. 85-99, 2012.
  Accès : http://dx.doi.org/10.1007/978-3-642-28891-3_9
  BibTeX

• Nicolas Brisebarre, Mioara Joldes, Peter Kornerup, Erik Martin-Dorel, Jean-Michel Muller. Augmented precision square roots, 2-D norms, and discussion on correctly rounding sqrt(x²+y²) (regular paper). Dans : IEEE Symposium on Computer Arithmetic (ARITH 2011), Tübingen, Germany, 25/07/11-27/07/11, IEEE : Institute of Electrical and Electronics Engineers, p. 23-30, 2011.
  Accès : http://dx.doi.org/10.1109/ARITH.2011.13
  BibTeX

• Nicolas Brisebarre, Milos Ercegovac, Nicolas Louvet, Erik Martin-Dorel, Jean-Michel Muller, Adrien Panhaleux. Implementing Decimal Floating-Point Arithmetic through Binary: Some Suggestions (poster). Dans : International Conference on Application-specific Systems Architectures and Processors (ASAP 2010), Rennes, 07/07/10-09/07/10, IEEE : Institute of Electrical and Electronics Engineers, p. 317-320, 2010.
  Accès : http://dx.doi.org/10.1109/ASAP.2010.5540969
  BibTeX

• Marc Daumas, David Lester, Erik Martin-Dorel, Annick Truffert. Stochastic formal correctness of numerical algorithms (regular paper). Dans : International Symposium on NASA Formal Methods (NFM 2009), Moffett Field, California, 06/04/09-08/04/09, NASA, p. 136-145, 2009.
  Accès : http://ti.arc.nasa.gov/m/events/nfm09/proceedings.pdf
  BibTeX

• Marc Daumas, Erik Martin-Dorel, Annick Truffert, Michel Ventou. A Formal Theory of Cooperative TU-Games (regular paper). Dans : Modeling Decisions for Artificial Intelligence (MDAI 2009), Awaji Island, Japan, 30/11/09-02/12/09, Springer, p. 81-91, 2009.
  Accès : http://dx.doi.org/10.1007/978-3-642-04820-3_8
  BibTeX

Conférences et workshops nationaux / National conference papers

• Marc Daumas, Erik Martin-Dorel, Annick Truffert. Bornes quasi-certaines sur l'accumulation d'erreurs infimes dans les systèmes hybrides (regular paper). Dans : Manifestation des Jeunes Chercheurs en Sciences et Technologies de l'Information et de la Communication (MajecSTIC 2009), Avignon, 16/11/09-18/11/09, Université d'Avignon, (en ligne), 2009.
  Accès : http://majecstic2009.univ-avignon.fr/Actes_MajecSTIC_RJCP/MajecSTIC/articles/1032.pdf
  BibTeX

Conférences sans actes publiés / Conference papers without published proceedings

• Erik Martin-Dorel, Sergei Soloviev. Cumulative Effects in Learning. Dans : Conference on Artificial Intelligence and Theorem Proving (AITP), Aussois, France, 25/03/18-30/03/18.
  Accès : http://aitp-conference.org/2018/aitp18-proceedings.pdf
  BibTeX

• Erik Martin-Dorel, Pierre Roux. A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations. Dans : Journées FAC 2017, Onera, Toulouse, 29/03/17-30/03/17.
  Accès : http://projects.laas.fr/IFSE/FAC/previous/journées-fac-2017/
  BibTeX

• Stéphane Le Roux, Erik Martin-Dorel, Jan-Georg Smaus. Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle. Dans : Journées FAC 2017, Onera, Toulouse, 29/03/17-30/03/17.
  Accès : http://projects.laas.fr/IFSE/FAC/previous/journ%C3%A9es-fac-2017/
  BibTeX

• Erik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. Dans : Journées FAC 2016, LAAS, Toulouse, 30/03/16-31/03/16.
  Accès : http://projects.laas.fr/IFSE/FAC/previous/journ%C3%A9es-fac-2016/
  BibTeX

• Erik Martin-Dorel, Guillaume Melquiond. CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq. Dans : The MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, CIRM, Luminy, Marseille, 11/01/16-15/01/16.
  Accès : http://scientific-events.weebly.com/1508.html
  BibTeX

• Erik Martin-Dorel. Formal proofs and certified computation in Coq. Dans : The French Symposium on Games - Theory and Applications, Université Paris Diderot, 26/05/15-30/05/15.
  Accès : http://www.games-symposium.fr/program
  BibTeX

• Erik Martin-Dorel. Univariate and Bivariate Integral Roots Certificates Based on Hensel Lifting. Dans : The Third Coq Workshop 2011, Nijmegen, Netherlands, 26/08/11-26/08/11, Bas Spitters (Eds.).
  Accès : http://www.cs.ru.nl/~spitters/coqw_files/program.html
  BibTeX

Rapports / Reports

• Erik Martin-Dorel, Sergei Soloviev. A Formal Study of Boolean Games with Random Formulas as Pay Functions. Rapport de recherche, IRIT/RR--2017--01--FR, IRIT, février 2017.
  Accès : https://www.irit.fr/publis/ACADIE/IRIT-RR-2017-01-FR.pdf
  BibTeX

• Erik Martin-Dorel, Guillaume Melquiond. Proving Tight Bounds on Univariate Expressions in Coq. Rapport de recherche, IRIT/RR--2014-09--FR, IRIT, novembre 2014.
  Accès : https://www.irit.fr/publis/ACADIE/IRIT-RR-2014-09-FR.pdf
  BibTeX

• Erik Martin-Dorel. Univariate and Bivariate Integral Roots Certificates Based on Hensel's Lifting. Rapport de recherche, RRLIP2011-1, LIP, Ecole Normale Supérieure de Lyon, mars 2011.
  Accès : http://hal.inria.fr/ensl-00575673/
  BibTeX

Thèses et habilitations / Ph.D Theses and Habilitation Theses

• Erik Martin-Dorel. Contributions to the Formal Verification of Arithmetic Algorithms. Thèse de doctorat, Ecole Normale Supérieure de Lyon, Lyon, septembre 2012.
  Accès : http://tel.archives-ouvertes.fr/tel-00745553/
  BibTeX