Accéder directement au contenu

Érik Martin-Dorel

33
Documents
Identifiants chercheurs

Présentation

Brought to you by HAL.
Brought to you by HAL.

Publications

Image document

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
14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Białystok, Poland. pp.1-18, ⟨10.4230/LIPIcs.ITP.2023.12⟩
Communication dans un congrès hal-04098856v2
Image document

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
14th International Conference on Interactive Theorem Proving (ITP 2023), Jul 2023, Bialystok, Poland. ⟨10.4230/LIPICS.ITP.2023.25⟩
Communication dans un congrès hal-04269882v1

Bel-Games: A Formal Theory of Games of Incomplete Information Based on Belief Functions in the Coq Proof Assistant

Hélène Fargier , Érik Martin-Dorel , Pierre Pomeret-Coquot
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
Communication dans un congrès hal-03709703v1
Image document

Games of Incomplete Information: A Framework Based on Belief Functions

Hélène Fargier , Érik Martin-Dorel , Pierre Pomeret-Coquot
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⟩
Communication dans un congrès hal-03382397v1
Image document

Jeux incomplets algébriques

Hélène Fargier , Érik Martin-Dorel , Pierre Pomeret-Coquot
Rencontres des Jeunes Chercheurs en Intelligence Artificielle (RJCIA 2021) @ Plate-Forme Intelligence Artificielle (PFIA 2021), Jul 2021, Bordeaux, France. pp.46-53
Communication dans un congrès hal-03298722v1
Image document

Primitive Floats in Coq

Guillaume Bertholon , Érik Martin-Dorel , Pierre Roux
ITP 2019, Interactive Theorem Proving, Sep 2019, PORTLAND, United States. ⟨10.4230/LIPIcs.ITP.2019.7⟩
Communication dans un congrès hal-02449191v1

Cumulative Effects in Learning

Érik Martin-Dorel , Sergei Soloviev
3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Mar 2018, Aussois, France
Communication dans un congrès hal-02982569v2
Image document

A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations

Érik Martin-Dorel , Pierre Roux
The 6th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2017), Jan 2017, Paris, France. pp.90 - 99, ⟨10.1145/3018610.3018622⟩
Communication dans un congrès hal-01510979v1

A Reflexive Tactic for Polynomial Positivity using Numerical Solvers and Floating-Point Computations (Journées FAC 2017)

Érik Martin-Dorel , Pierre Roux
Journées FAC 2017, Groupe IFSE du RTRA STAE, Mar 2017, Toulouse, France
Communication dans un congrès hal-03131862v1

An Existence Theorem of Nash Equilibrium in Coq and Isabelle

Stéphane Le Roux , Érik Martin-Dorel , Jan-Georg Smaus
8th International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2017), Sep 2017, Rome, Italy. pp.46-60, ⟨10.4204/EPTCS.256.4⟩
Communication dans un congrès hal-03434697v1

Formalization of an existence theorem of Nash equilibrium in Coq and Isabelle (Journées FAC 2017)

Stéphane Le Roux , Érik Martin-Dorel , Jan-Georg Smaus
Journées FAC 2017, Groupe IFSE du RTRA STAE, Mar 2017, Toulouse, France
Communication dans un congrès hal-03131861v1

CoqInterval: A Toolbox for Proving Non-linear Univariate Inequalities in Coq

Érik Martin-Dorel , Guillaume Melquiond
MAP 2016 conference on Effective Analysis: Foundations, Implementations, Certification, Jan 2016, Marseille, France
Communication dans un congrès hal-03155045v1
Image document

A Formal Study of Boolean Games with Random Formulas as Payoff Functions

Érik Martin-Dorel , Sergei Soloviev
22nd International Conference on Types for Proofs and Programs (TYPES 2016), May 2016, Novi Sad, Serbia. pp.1-22, ⟨10.4230/LIPIcs.TYPES.2016.14⟩
Communication dans un congrès hal-02651342v1

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq (Journées FAC 2016)

Érik Martin-Dorel , Guillaume Melquiond
Journées Formalisation des Activités Concurrentes (FAC 2016), Groupe IFSE du RTRA STAE (Réseau Thématique de Recherche Avancée « Sciences et Technologies pour l’Aéronautique et l’Espace » de Toulouse), Mar 2016, Toulouse, France
Communication dans un congrès hal-03176418v1

Formal proofs and certified computation in Coq (The French Symposium on Games - Theory and Applications, Université Paris Diderot, 26/05/15-30/05/15)

Érik Martin-Dorel
French Symposium on Games - Theory and Applications 2015 (Dedicated to the memory of John Nash), May 2015, Paris, France
Communication dans un congrès hal-03193111v1
Image document

Certified, Efficient and Sharp Univariate Taylor Models in COQ

Érik Martin-Dorel , Micaela Mayero , Ioana Pasca , Laurence Rideau , Laurent Théry
SYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania
Communication dans un congrès hal-00845791v2
Image document

Rigorous Polynomial Approximation using Taylor Models in Coq

Nicolas Brisebarre , Mioara Maria Joldes , Érik Martin-Dorel , Micaela Mayero , Jean-Michel Muller
Fourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15
Communication dans un congrès ensl-00653460v2
Image document

Augmented precision square roots, 2-D norms, and discussion on correctly rounding {x^2+y^2}

Nicolas Brisebarre , Mioara Maria Joldes , Peter Kornerup , Érik Martin-Dorel , Jean-Michel Muller
20th IEEE Symposium on Computer Arithmetic (ARITH-20), Jul 2011, Tübingen, Germany. pp.23-30, ⟨10.1109/ARITH.2011.13⟩
Communication dans un congrès ensl-00545591v2

Formalization of Hensel's lemma in Coq

Érik Martin-Dorel
TYPES 2010: The 17th Workshop on Types for Proofs and Programs, Oct 2010, Warsaw, Poland
Communication dans un congrès ensl-00560449v1
Image document

Implementing decimal floating-point arithmetic through binary: some suggestions

Nicolas Brisebarre , Milos Ercegovac , Nicolas Louvet , Érik Martin-Dorel , Jean-Michel Muller
21st IEEE International Conference on Application-specific Systems, Architectures and Processors (ASAP 2010), Jul 2010, Rennes, France. pp.317-320, ⟨10.1109/ASAP.2010.5540969⟩
Communication dans un congrès ensl-00463353v2
Image document

Coq Community Survey 2022: Summary of Results

Ana de Almeida Borges , Jean-Rémy Falleri , Jim Fehrle , Emilio Jesús Gallego Arias , Érik Martin-Dorel
13th installment of the Coq Workshop series (Coq workshop 2022), Aug 2022, Haifa, Israel.
Document associé à des manifestations scientifiques hal-03914602v1
Image document

Contributions to the Formal Verification of Arithmetic Algorithms

Erik Martin-Dorel
Other [cs.OH]. Ecole normale supérieure de lyon - ENS LYON, 2012. English. ⟨NNT : 2012ENSL0742⟩
Thèse tel-00745553v1