Accueil du site > Français > Productions scientifiques > Publications
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
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/2016-26/05/2016, Herman Geuvers, Silvia Ghilezan, Jelena Ivetic (Eds.), Schloss Dagstuhl Leibniz-Zentrum fur Informatik, LIPICS, 2018 (à paraître).
Résumé
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/2017-22/09/2017, Vol. 256, Electronic Proceedings in Theoretical Computer Science, p. 46-60, septembre 2017.
Accès : http://dx.doi.org/10.4204/EPTCS.256.4
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/2017-17/01/2017, ACM, 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/2013-26/09/2013, IEEE, 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/2012-05/04/2012, 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/2011-27/07/2011, IEEE, 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/2010-09/07/2010, IEEE, 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/2009-08/04/2009, 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/2009-02/12/2009, Springer, p. 81-91, 2009.
Accès : http://dx.doi.org/10.1007/978-3-642-04820-3_8
BibTeX
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/2009-18/11/2009, Université d'Avignon, (en ligne), 2009.
Accès : http://majecstic2009.univ-avignon.fr/Actes_MajecSTIC_RJCP/MajecSTIC/articles/1032.pdf
BibTeX
Erik Martin-Dorel, Sergei Soloviev. Cumulative Effects in Learning. Dans : Conference on Artificial Intelligence and Theorem Proving (AITP), Aussois, France, 25/03/2018-30/03/2018.
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/2017-30/03/2017.
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/2017-30/03/2017.
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/2016-31/03/2016.
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/2016-15/01/2016.
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/2015-30/05/2015.
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/2011-26/08/2011, Bas Spitters (Eds.).
Accès : http://www.cs.ru.nl/~spitters/coqw_files/program.html
BibTeX
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
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