Publications de Erik MARTIN-DOREL
Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux
Enabling Floating-Point Arithmetic in the Coq Proof Assistant
Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩
Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel
Games of Incomplete Information: a Framework Based on Belief Functions
International Journal of Approximate Reasoning, 2022, 151, pp.182-204. ⟨10.1016/j.ijar.2022.09.010⟩
Erik Martin-Dorel, Guillaume Melquiond
Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq
Dans : Journal of Automated Reasoning, Springer-Verlag, Heidelberg, Allemagne, Vol. 57 N. 3, p. 187-217, octobre 2016.
Résumé Accès : http://dx.doi.org/10.1007/s10817-015-9350-4 – http://www.irit.fr/publis/ACADIE/CoqInterval-JAR.pdf – https://oatao.univ-toulouse.fr/16862/
BibTeXErik 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, Heidelberg, Allemagne, Vol. 54 N. 1, p. 1-29, janvier 2015.
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.
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.
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
Lessons for Interactive Theorem Proving Researchers from a Survey of Coq Users
14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Białystok, Poland. pp.1-18, ⟨10.4230/LIPIcs.ITP.2023.12⟩
Hélène Fargier, Érik Martin-Dorel, Pierre Pomeret-Coquot
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
Ecole Jeunes Chercheuses et Chercheurs en Informatique Mathématique, Maison de la Modélisation, de la Simulation et des Interactions [MSI], Jun 2022, Nice, France
Hélène Fargier, Érik Martin-Dorel, Pierre Pomeret-Coquot
Games of Incomplete Information: A Framework Based on Belief Functions
16th European Conference on Symbolic and Quantitative Approaches to Reasoning with Uncertainty (ECSQARU 2021), Sep 2021, Prague, Czech Republic. pp.328-341, ⟨10.1007/978-3-030-86772-0_24⟩
Hélène Fargier, Érik Martin-Dorel, Pierre Pomeret-Coquot
Jeux incomplets algébriques
Rencontres des Jeunes Chercheurs en Intelligence Artificielle (RJCIA 2021) @ Plate-Forme Intelligence Artificielle (PFIA 2021), Jul 2021, Bordeaux, France. pp.46-53
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⟩
Érik Martin-Dorel, Sergei Soloviev
Cumulative Effects in Learning
3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Mar 2018, Aussois, France
Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus
An Existence Theorem of Nash Equilibrium in Coq and Isabelle
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017), Sep 2017, Rome, Italy. pp.46-60, ⟨10.4204/EPTCS.256.4⟩
Stéphane Le Roux, Érik Martin-Dorel, Jan-Georg Smaus
Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle (Journées FAC 2017)
Journées FAC 2017, Groupe IFSE du RTRA STAE, Mar 2017, Toulouse, France
Érik Martin-Dorel, Pierre Roux
A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations (Journées FAC 2017)
Journées FAC 2017, Groupe IFSE du RTRA STAE, Mar 2017, Toulouse, France
É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⟩
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/
BibTeXErik 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
BibTeXFormal proofs and certified computation in Coq
Dans : The French Symposium on Games – Theory and Applications, Université Paris Diderot, 26/05/15-30/05/15.
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.
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
BibTeXNicolas 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.
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
BibTeXNicolas 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.
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
BibTeXMarc 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
BibTeXMarc 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
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
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.
Pierre Pomeret-Coquot, Hélène Fargier, Érik Martin-Dorel
Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant
2023