Journal articles
2023
- titre
- Le dilemme du fabricant de tables
- auteur
- Sylvie Boldo, Nicolas Brisebarre, Jean-Michel Muller
- article
- La Recherche, 2023, 572
- Accès au bibtex
-
- titre
- Floating-point arithmetic
- auteur
- Sylvie Boldo, Claude-Pierre Jeannerod, Guillaume Melquiond, Jean-Michel Muller
- article
- Acta Numerica, 2023, 32, pp.203-290. ⟨10.1017/S0962492922000101⟩
- DOI
- DOI : 10.1017/S0962492922000101
- Accès au texte intégral et bibtex
-
2022
- titre
- A Coq Formalization of Lebesgue Integration of Nonnegative Functions
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- Journal of Automated Reasoning, 2022, 66, pp.175-213. ⟨10.1007/s10817-021-09612-0⟩
- DOI
- DOI : 10.1007/s10817-021-09612-0
- Accès au texte intégral et bibtex
-
- titre
- Bounding the Round-Off Error of the Upwind Scheme for Advection
- auteur
- Louise Ben Salem-Knapp, Sylvie Boldo, William Weens
- article
- IEEE Transactions on Emerging Topics in Computing, 2022, 10 (3), ⟨10.1109/TETC.2022.3191472⟩
- DOI
- DOI : 10.1109/TETC.2022.3191472
- Accès au texte intégral et bibtex
-
2021
- titre
- Emulating round-to-nearest ties-to-zero "augmented" floating-point operations using round-to-nearest ties-to-even arithmetic
- auteur
- Sylvie Boldo, Christoph Q. Lauter, Jean-Michel Muller
- article
- IEEE Transactions on Computers, 2021, 70 (7), pp.1046 - 1058. ⟨10.1109/TC.2020.3002702⟩
- DOI
- DOI : 10.1109/TC.2020.3002702
- Accès au texte intégral et bibtex
-
2020
- titre
- Optimal Inverse Projection of Floating-Point Addition
- auteur
- Diane Gallois-Wong, Sylvie Boldo, Pascal Cuoq
- article
- Numerical Algorithms, In press, 83 (3), pp.957--986. ⟨10.1007/s11075-019-00711-z⟩
- DOI
- DOI : 10.1007/s11075-019-00711-z
- Accès au texte intégral et bibtex
-
2019
- titre
- Round-off error and exceptional behavior analysis of explicit Runge-Kutta methods
- auteur
- Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
- article
- IEEE Transactions on Computers, 2019, ⟨10.1109/TC.2019.2917902⟩
- DOI
- DOI : 10.1109/TC.2019.2917902
- Accès au texte intégral et bibtex
-
2017
- titre
- On the robustness of the 2Sum and Fast2Sum algorithms
- auteur
- Sylvie Boldo, Stef Graillat, Jean-Michel Muller
- article
- ACM Transactions on Mathematical Software, 2017, 44 (1)
- Accès au texte intégral et bibtex
-
2016
- titre
- Formalization of Real Analysis: A Survey of Proof Assistants and Libraries
- auteur
- Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
- article
- Mathematical Structures in Computer Science, 2016, 26 (7), pp.1196-1233. ⟨10.1017/S0960129514000437⟩
- DOI
- DOI : 10.1017/S0960129514000437
- Accès au texte intégral et bibtex
-
2015
- titre
- Verified Compilation of Floating-Point Computations
- auteur
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
- article
- Journal of Automated Reasoning, 2015, 54 (2), pp.135-163. ⟨10.1007/s10817-014-9317-x⟩
- DOI
- DOI : 10.1007/s10817-014-9317-x
- Accès au texte intégral et bibtex
-
- titre
- Coquelicot: A User-Friendly Library of Real Analysis for Coq
- auteur
- Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
- article
- Mathematics in Computer Science, 2015, 9 (1), pp.41-62. ⟨10.1007/s11786-014-0181-1⟩
- DOI
- DOI : 10.1007/s11786-014-0181-1
- Accès au texte intégral et bibtex
-
2014
- titre
- Trusting computations: a mechanized proof from partial differential equations to actual program
- auteur
- Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
- article
- Computers & Mathematics with Applications, 2014, 68 (3), pp.28. ⟨10.1016/j.camwa.2014.06.004⟩
- DOI
- DOI : 10.1016/j.camwa.2014.06.004
- Accès au texte intégral et bibtex
-
- titre
- Des ordinateurs capables de calculer plus juste
- auteur
- Jean-Michel Muller, Sylvie Boldo
- article
- La Recherche, 2014, pp.46-53
- Accès au bibtex
-
2013
- titre
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- auteur
- Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
- article
- Journal of Automated Reasoning, 2013, 50 (4), pp.423-456. ⟨10.1007/s10817-012-9255-4⟩
- DOI
- DOI : 10.1007/s10817-012-9255-4
- Accès au texte intégral et bibtex
-
2011
- titre
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- auteur
- Sylvie Boldo, Claude Marché
- article
- Mathematics in Computer Science, 2011, 5, pp.377-393
- Accès au texte intégral et bibtex
-
- titre
- Proofs of numerical programs when the compiler optimizes
- auteur
- Sylvie Boldo, Thi Minh Tuyen Nguyen
- article
- Innovations in Systems and Software Engineering, 2011, 7, pp.151-160
- Accès au texte intégral et bibtex
-
- titre
- Exact and Approximated error of the FMA
- auteur
- Sylvie Boldo, Jean-Michel Muller
- article
- IEEE Transactions on Computers, 2011, 60 (2), pp.157-164. ⟨10.1109/TC.2010.139⟩
- DOI
- DOI : 10.1109/TC.2010.139
- Accès au texte intégral et bibtex
-
2010
- titre
- Un algorithme de découpe de gâteau
- auteur
- Sylvie Boldo
- article
- Interstices, 2010
- Accès au bibtex
-
- titre
- C'est la faute à l'ordinateur !
- auteur
- Sylvie Boldo
- article
- Interstices, 2010
- Accès au bibtex
-
2009
- titre
- Formally Verified Argument Reduction with a Fused Multiply-Add
- auteur
- Sylvie Boldo, Marc Daumas, Ren-Cang Li
- article
- IEEE Transactions on Computers, 2009, 58 (8), pp.1139-1145. ⟨10.1109/TC.2008.216⟩
- DOI
- DOI : 10.1109/TC.2008.216
- Accès au texte intégral et bibtex
-
- titre
- Demandez le programme
- auteur
- Sylvie Boldo
- article
- Interstices, 2009
- Accès au bibtex
-
- titre
- Kahan's algorithm for a correct discriminant computation at last formally proven
- auteur
- Sylvie Boldo
- article
- IEEE Transactions on Computers, 2009, 58 (2), pp.220-225. ⟨10.1109/TC.2008.200⟩
- DOI
- DOI : 10.1109/TC.2008.200
- Accès au texte intégral et bibtex
-
- titre
- Computing predecessor and successor in rounding to nearest
- auteur
- Siegfried Rump, Paul Zimmermann, Sylvie Boldo, Guillaume Melquiond
- article
- BIT Numerical Mathematics, 2009, 49 (2), pp.419-431. ⟨10.1007/s10543-009-0218-z⟩
- DOI
- DOI : 10.1007/s10543-009-0218-z
- Accès au texte intégral et bibtex
-
- titre
- Floats & Ropes: a case study for formal numerical program verification
- auteur
- Sylvie Boldo
- article
- Lecture Notes in Computer Science, 2009, 36th International Colloquium on Automata, Languages and Programming, 5556, pp.91--102. ⟨10.1007/978-3-642-02930-1_8⟩
- DOI
- DOI : 10.1007/978-3-642-02930-1_8
- Accès au bibtex
-
2008
- titre
- Pourquoi mon ordinateur calcule-t-il faux ?
- auteur
- Sylvie Boldo, Joanna Jongwane
- article
- Interstices, 2008
- Accès au bibtex
-
- titre
- Idée reçue : L’informatique, ce n’est pas pour les filles
- auteur
- Sylvie Boldo, Thierry Viéville
- article
- Interstices, 2008
- Accès au bibtex
-
- titre
- Emulation of a FMA and correctly-rounded sums: proved algorithms using rounding to odd
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- IEEE Transactions on Computers, 2008, 57 (4), pp.462-471. ⟨10.1109/TC.2007.70819⟩
- DOI
- DOI : 10.1109/TC.2007.70819
- Accès au texte intégral et bibtex
-
2004
- titre
- A simple test qualifying the accuracy of Horner's rule for polynomials
- auteur
- Sylvie Boldo, Marc Daumas
- article
- Numerical Algorithms, 2004, 37 (1-4), pp.45-60. ⟨10.1023/B:NUMA.0000049487.98618.61⟩
- DOI
- DOI : 10.1023/B:NUMA.0000049487.98618.61
- Accès au texte intégral et bibtex
-
2003
- titre
- Properties of two's complement floating point notations
- auteur
- Sylvie Boldo, Marc Daumas
- article
- International Journal on Software Tools for Technology Transfer, 2003, 5 (2-3), pp.237-246. ⟨10.1007/s10009-003-0120-y⟩
- DOI
- DOI : 10.1007/s10009-003-0120-y
- Accès au texte intégral et bibtex
-
Conference papers
2025
- titre
- Generation of Pathological Cases for Rounding Errors
- auteur
- Sylvie Boldo, David Hamelin, Thibault Hilaire, Pierre-Yves Piriou
- article
- RAIM Meeting 2025: 16th Rencontres de l'Arithmétique en Informatique Mathématique – A Tribute to Jean-Michel Muller, Nov 2025, Lyon, France
- Accès au bibtex
-
2024
- titre
- Teaching Divisibility and Binomials with Coq
- auteur
- Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin
- article
- 13th International Workshop on Theorem proving components for Educational software - ThEdu 2024, Julien Narboux; Walther Neuper; Pedro Quaresma, Jul 2024, Nancy, France. pp.124 - 139, ⟨10.4204/EPTCS.419.8⟩
- DOI
- DOI : 10.4204/EPTCS.419.8
- Accès au texte intégral et bibtex
-
2023
- titre
- A Coq Formalization of Lebesgue Induction Principle and Tonelli's Theorem
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
- article
- 25th International Symposium on Formal Methods (FM 2023), Mar 2023, Lübeck, Germany. pp.39--55, ⟨10.1007/978-3-031-27481-7_4⟩
- DOI
- DOI : 10.1007/978-3-031-27481-7_4
- Accès au texte intégral et bibtex
-
2021
- titre
- Some Formal Tools for Computer Arithmetic: Flocq and Gappa
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- ARITH 2021 - 28th IEEE International Symposium on Computer Arithmetic, Jun 2021, Online, Italy
- Accès au texte intégral et bibtex
-
2020
- titre
- A Correctly-Rounded Fixed-Point-Arithmetic Dot-Product Algorithm
- auteur
- Sylvie Boldo, Diane Gallois-Wong, Thibault Hilaire
- article
- ARITH 2020 - IEEE 27th Symposium on Computer Arithmetic, Jun 2020, Portland, United States. pp.9-16, ⟨10.1109/ARITH48897.2020.00011⟩
- DOI
- DOI : 10.1109/ARITH48897.2020.00011
- Accès au texte intégral et bibtex
-
2018
- titre
- A Formally-Proved Algorithm to Compute the Correct Average of Decimal Floating-Point Numbers
- auteur
- Sylvie Boldo, Florian Faissole, Vincent Tourneur
- article
- 25th IEEE Symposium on Computer Arithmetic, Jun 2018, Amherst, MA, United States
- Accès au texte intégral et bibtex
-
- titre
- A Coq formalization of digital filters
- auteur
- Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire
- article
- CICM 2018 - 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. pp.87--103, ⟨10.1007/978-3-319-96812-4_8⟩
- DOI
- DOI : 10.1007/978-3-319-96812-4_8
- Accès au texte intégral et bibtex
-
2017
- titre
- A Coq formal proof of the Lax–Milgram theorem
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- 6th ACM SIGPLAN Conference on Certified Programs and Proofs, Jan 2017, Paris, France. ⟨10.1145/3018610.3018625⟩
- DOI
- DOI : 10.1145/3018610.3018625
- Accès au texte intégral et bibtex
-
- titre
- Formal Verification of a Floating-Point Expansion Renormalization Algorithm
- auteur
- Sylvie Boldo, Mioara Joldes, Jean-Michel Muller, Valentina Popescu
- article
- 8th International Conference on Interactive Theorem Proving (ITP'2017), Sep 2017, Brasilia, Brazil
- Accès au texte intégral et bibtex
-
- titre
- Preuve formelle du théorème de Lax–Milgram
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- 16èmes journées Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2017, Montpellier, France
- Accès au texte intégral et bibtex
-
- titre
- Round-off Error Analysis of Explicit One-Step Numerical Integration Methods
- auteur
- Sylvie Boldo, Florian Faissole, Alexandre Chapoutot
- article
- 24th IEEE Symposium on Computer Arithmetic, Jul 2017, London, United Kingdom. ⟨10.1109/ARITH.2017.22⟩
- DOI
- DOI : 10.1109/ARITH.2017.22
- Accès au texte intégral et bibtex
-
2016
- titre
- Iterators: where folds fail
- auteur
- Sylvie Boldo
- article
- Workshop on High-Consequence Control Verification, Jul 2016, Toronto, Canada
- Accès au texte intégral et bibtex
-
- titre
- Computing a correct and tight rounding error bound using rounding-to-nearest
- auteur
- Sylvie Boldo
- article
- 9th International Workshop on Numerical Software Verification, Jul 2016, Toronto, Canada
- Accès au texte intégral et bibtex
-
2015
- titre
- Stupid is as Stupid Does: Taking the Square Root of the Square of a Floating-Point Number
- auteur
- Sylvie Boldo
- article
- Seventh and Eighth International Workshop on Numerical Software Verification, Apr 2015, Seattle, WA, United States. pp.50--55
- Accès au texte intégral et bibtex
-
- titre
- Formal Verification of Programs Computing the Floating-Point Average
- auteur
- Sylvie Boldo
- article
- 17th International Conference on Formal Engineering Methods, Nov 2015, Paris, France. pp.17-32
- Accès au texte intégral et bibtex
-
2014
- titre
- Formal verification of tricky numerical computations
- auteur
- Sylvie Boldo
- article
- 16th GAMM-IMACS International Symposium on Scientific Computing, Computer Arithmetic and Validated Numerics, Sep 2014, Würzburg, Germany. pp.39
- Accès au texte intégral et bibtex
-
2013
- titre
- A Formally-Verified C Compiler Supporting Floating-Point Arithmetic
- auteur
- Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, Guillaume Melquiond
- article
- Arith - 21st IEEE Symposium on Computer Arithmetic, Apr 2013, Austin, United States. pp.107-115
- Accès au texte intégral et bibtex
-
- titre
- How to Compute the Area of a Triangle: a Formal Revisit
- auteur
- Sylvie Boldo
- article
- 21st IEEE International Symposium on Computer Arithmetic, Apr 2013, Austin, TX, United States. pp.91-98, ⟨10.1109/ARITH.2013.29⟩
- DOI
- DOI : 10.1109/ARITH.2013.29
- Accès au texte intégral et bibtex
-
2012
- titre
- Improving Real Analysis in Coq: a User-Friendly Approach to Integrals and Derivatives
- auteur
- Sylvie Boldo, Catherine Lelay, Guillaume Melquiond
- article
- CPP - 2nd International Conference on Certified Programs and Proofs - 2012, Dec 2012, Kyoto, Japan. pp.289-304, ⟨10.1007/978-3-642-35308-6_22⟩
- DOI
- DOI : 10.1007/978-3-642-35308-6_22
- Accès au texte intégral et bibtex
-
- titre
- Arithmétique des ordinateurs et preuves formelles
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- École des Jeunes Chercheurs en Informatique Mathématique, GDR Informatique Mathématique, Mar 2012, Rennes, France. pp.1-30
- Accès au texte intégral et bibtex
-
2011
- titre
- Flocq: A Unified Library for Proving Floating-point Algorithms in Coq
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- Proceedings of the 20th IEEE Symposium on Computer Arithmetic, Jul 2011, Tübingen, Germany. pp.243-252, ⟨10.1109/ARITH.2011.40⟩
- DOI
- DOI : 10.1109/ARITH.2011.40
- Accès au texte intégral et bibtex
-
2010
- titre
- Formal verification of numerical programs: from C annotated programs to Coq proofs
- auteur
- Sylvie Boldo
- article
- NSV-3: Third International Workshop on Numerical Software Verification, Jul 2010, Edinburgh, Scotland, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Formal proof of a wave equation resolution scheme: the method error
- auteur
- Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis
- article
- ITP'10 - Interactive Theorem Proving, Jul 2010, Edinburgh, United Kingdom. pp.147-162, ⟨10.1007/978-3-642-14052-5_12⟩
- DOI
- DOI : 10.1007/978-3-642-14052-5_12
- Accès au texte intégral et bibtex
-
- titre
- Hardware-independent proofs of numerical programs
- auteur
- Sylvie Boldo, Thi Minh Tuyen Nguyen
- article
- Second NASA Formal Methods Symposium (NFM 2010), NASA, Apr 2010, Washington D.C., United States. pp.14-23
- Accès au texte intégral et bibtex
-
2009
- titre
- Combining Coq and Gappa for Certifying Floating-Point Programs
- auteur
- Sylvie Boldo, Jean-Christophe Filliâtre, Guillaume Melquiond
- article
- 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, Jul 2009, Grand Bend, Ontario, Canada. pp.59-74, ⟨10.1007/978-3-642-02614-0_10⟩
- DOI
- DOI : 10.1007/978-3-642-02614-0_10
- Accès au texte intégral et bibtex
-
2008
- titre
- Formal proof for delayed finite field arithmetic using floating point operators
- auteur
- Sylvie Boldo, Marc Daumas, Pascal Giorgi
- article
- 8th Conference on Real Numbers and Computers, Jul 2008, Saint Jacques de Compostelle, Spain. pp.113-122
- Accès au texte intégral et bibtex
-
2006
- titre
- Provably Faithful Evaluation of Polynomials
- auteur
- Sylvie Boldo, César Muñoz
- article
- 21st Annual ACM Symposium on Applied Computing, Apr 2006, Dijon, France
- Accès au texte intégral et bibtex
-
2005
- titre
- Some Functions Computable with a Fused-mac
- auteur
- Sylvie Boldo, Jean-Michel Muller
- article
- 17th IEEE Symposium on Computer Arithmetic, Jun 2005, Cape Cod, Massachusetts, USA, pp.52-58
- Accès au texte intégral et bibtex
-
- titre
- When double rounding is odd
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- 17th IMACS World Congress, Jul 2005, Paris, France. pp.11
- Accès au texte intégral et bibtex
-
2003
- titre
- Theorems on Efficient Argument Reductions
- auteur
- Ren Cang Li, Sylvie Boldo, Marc Daumas
- article
- 16th IEEE Symposium on Computer Arithmetic, 2003, Santiago de Compostela, Spain. pp.129-136, ⟨10.1109/ARITH.2003.1207670⟩
- DOI
- DOI : 10.1109/ARITH.2003.1207670
- Accès au texte intégral et bibtex
-
2002
- titre
- Properties of the subtraction valid for any floating point system
- auteur
- Sylvie Boldo, Marc Daumas
- article
- 7th International Workshop on Formal Methods for Industrial Critical Systems, 2002, Málaga, Spain. pp.137-149
- Accès au texte intégral et bibtex
-
Book sections
2014
- titre
- Même les ordinateurs font des erreurs !
- auteur
- Sylvie Boldo
- article
- Martin Andler; Liliane Bel; Sylvie Benzoni-Gavage; Thierry Goudon; Cyril Imbert; Antoine Rousseau. Brèves de maths, Nouveau Monde Editions, pp.136-137, 2014, 978-2-36583-896-2
- Accès au bibtex
-
2013
- titre
- Arithmétique des ordinateurs et preuves formelles
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- Informatique mathématique : Une photographie en 2013, 2013
- Accès au bibtex
-
Habilitation à diriger des recherches
2014
- titre
- Deductive Formal Verification: How To Make Your Floating-Point Programs Behave
- auteur
- Sylvie Boldo
- article
- Computer Arithmetic. Université Paris-Sud, 2014
- Accès au texte intégral et bibtex
-
Other publications
2015
- titre
- « Structures : organisation, complexité, dynamique » des mot-clés au sens inattendu
- auteur
- Thierry Viéville, Sylvie Boldo, Florent Masseglia, Pierre Bernhard
- article
- 2015
- Accès au bibtex
-
2010
- titre
- L'informatique
- auteur
- Sylvie Boldo
- article
- 2010
- Accès au bibtex
-
Books
2018
- titre
- Actes des Journées Francophones des Langages Applicatifs 2018
- auteur
- Sylvie Boldo, Nicolas Magaud
- article
- INRIA, 2018
- Accès au bibtex
-
2017
- titre
- Computer Arithmetic and Formal Proofs
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- ISTE Press - Elsevier, pp.326, 2017, 9781785481123
- Accès au bibtex
-
2011
- titre
- Une introduction à la science informatique pour les enseignants de la discipline en lycée
- auteur
- Gilles Dowek, Jean-Pierre Archambault, Emmanuel Baccelli, Sylvie Boldo, Denis Bouhineau, Patrick Cegielski, Thomas Heide Clausen, Irène Guessarian, Stéphane Lopes, Laurent Mounier, Benjamin Nguyen, Franck Quessette, Anne Rasse, Brigitte Rozoy, Claude Timsit, Thierry Viéville, Jean-Marc Vincent
- article
- Gilles Dowek. CRDP Paris, pp.376, 2011, Repères pour agir (RPA disciplines & compétences), Christine Moulin, 978-2-86631-188-9
- Accès au bibtex
-
Poster communications
2010
- titre
- Formal proofs of numerical programs
- auteur
- Nguyen Thi Minh Tuyen, Sylvie Boldo, Claude Marché
- article
- Forum Digitéo, Oct 2010, Palaiseau, France
- Accès au texte intégral et bibtex
-
Proceedings
2019
- titre
- Proceedings of the 26th Symposium on Computer Arithmetic (ARITH 2019)
- auteur
- Sylvie Boldo, Martin Langhammer
- article
- ARITH 2019 - 26th IEEE Symposium on Computer Arithmetic, Jun 2019, Kyoto, IEEE, 2019, 978-1-7281-3367-6. ⟨10.1109/ARITH.2019.00005⟩
- DOI
- DOI : 10.1109/ARITH.2019.00005
- Accès au bibtex
-
2018
- titre
- Journées Francophones des Langages Applicatifs 2018
- auteur
- Sylvie Boldo, Nicolas Magaud
- article
- Sylvie Boldo; Nicolas Magaud. Journées Francophones des Langages Applicatifs 2018, Jan 2018, Banyuls-sur-Mer, France. publié par les auteurs, 2018
- Accès au texte intégral et bibtex
-
2017
- titre
- 10th International Workshop on Numerical Software Verification
- auteur
- Alessandro Abate, Sylvie Boldo
- article
- 10th International Workshop on Numerical Software Verification, France. Springer, 2017
- Accès au bibtex
-
- titre
- Vingt-huitièmes Journées Francophones des Langages Applicatifs
- auteur
- Sylvie Boldo, Julien Signoles
- article
- Vingt-huitièmes Journées Francophones des Langages Applicatifs, Gourette, France. Published by the authors, 2017
- Accès au bibtex
-
Reports
2026
- titre
- Code of Conduct of the GDR-IFM
- auteur
- Miriam Backens, Magali Bardet, Jérémie Bettinelli, Marie van den Bogaard, Sylvie Boldo, Mathilde Bouvel, Pierre Clairambault, Maxime Folschette, Léo Gayral, Xavier Goaoc, Eleonora Guerrini, Timothée Martinod, Élodie Puybareau, Mathilde Vernet
- article
- GDR-IFM. 2026
- Accès au texte intégral et bibtex
-
2025
- titre
- A Rocq Formalization of Monomial and Graded Orders
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero
- article
- RR-9604, INRIA. 2025, pp.17
- Accès au texte intégral et bibtex
-
- titre
- A Rocq Formalization of Simplicial Lagrange Finite Elements
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
- article
- RR-9590, INRIA. 2025, pp.63
- Accès au texte intégral et bibtex
-
2024
- titre
- Teaching Divisibility and Binomials with Coq
- auteur
- Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin
- article
- RR-9547, Inria. 2024, pp.13
- Accès au texte intégral et bibtex
-
2023
- titre
- Lebesgue Induction and Tonelli's Theorem in Coq
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
- article
- [Research Report] RR-9457, Institut National de Recherche en Informatique et en Automatique (INRIA). 2023, pp.17
- Accès au texte intégral et bibtex
-
2022
- titre
- A Coq Formalization of the Bochner integral
- auteur
- Sylvie Boldo, François Clément, Louise Leclerc
- article
- [Research Report] RR-9456, Inria Saclay - Île de France; Inria de Paris. 2022
- Accès au texte intégral et bibtex
-
2021
- titre
- A Coq Formalization of Lebesgue Integration of Nonnegative Functions
- auteur
- Sylvie Boldo, François Clément, Florian Faissole, Vincent Martin, Micaela Mayero
- article
- [Research Report] RR-9401, Inria, France. 2021, pp.38
- Accès au texte intégral et bibtex
-
2013
- titre
- Médiation Scientifique : une facette de nos métiers de la recherche
- auteur
- Antoine Rousseau, Aurélie Darnaud, Brice Goglin, Céline Acharian, Christine Leininger, Christophe Godin, Clarisse Holik, Claude Kirchner, Diane Rives, Elodie Darquie, Erwan Kerrien, Fabrice Neyret, Florent Masseglia, Florian Dufour, Gérard Berry, Gilles Dowek, Hélène Robak, Hélène Xypas, Irina Illina, Isabelle Gnaedig, Joanna Jongwane, Jocelyne Ehrel, Laurent Viennot, Laure Guion, Lisette Calderan, Lola Kovacic, Marie Collin, Marie-Agnès Enard, Marie-Hélène Comte, Martin Quinson, Martine Olivi, Mathieu Giraud, Mathilde Dorémus, Mia Ogouchi, Muriel Droin, Nathalie Lacaux, Nicolas P. Rougier, Nicolas Roussel, Pascal Guitton, Pierre Peterlongo, Rose-Marie Cornus, Simon Vandermeersch, Sophie Maheo, Sylvain Lefebvre, Sylvie Boldo, Thierry Viéville, Véronique Poirel, Aline Chabreuil, Arnaud Fischer, Claude Farge, Claude Vadel, Isabelle Astic, Jean-Pierre Dumont, Loic Féjoz, Patrick Rambert, Pierre Paradinas, Sophie de Quatrebarbes, Stéphane Laurent
- article
- [Interne] Inria. 2013, pp.34
- Accès au texte intégral et bibtex
-
2004
- titre
- Some Functions Computable with a Fused-mac
- auteur
- Sylvie Boldo, Jean-Michel Muller
- article
- [Research Report] LIP RR-2004-41, Laboratoire de l'informatique du parallélisme. 2004, 2+10p
- Accès au texte intégral et bibtex
-
- titre
- When double rounding is odd
- auteur
- Sylvie Boldo, Guillaume Melquiond
- article
- [Research Report] LIP RR-2004-48, Laboratoire de l'informatique du parallélisme. 2004, 2+7p
- Accès au texte intégral et bibtex
-
2003
- titre
- A simple test qualifying the accuracy of Horner's rule for polynomials
- auteur
- Sylvie Boldo, Marc Daumas
- article
- [Research Report] LIP RR-2003-01, Laboratoire de l'informatique du parallélisme. 2003, 2+39p
- Accès au texte intégral et bibtex
-
2002
- titre
- Necessary and sufficient conditions for exact floating point operations
- auteur
- Marc Daumas, Sylvie Boldo
- article
- [Research Report] RR-4644, LIP RR-2002-44, INRIA, LIP. 2002
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, ...
2025
- titre
- A Rocq Formalization of Monomial and Graded Orders
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero
- article
- 2025
- Accès au texte intégral et bibtex
-
- titre
- A Rocq Formalization of Simplicial Lagrange Finite Elements
- auteur
- Sylvie Boldo, François Clément, Vincent Martin, Micaela Mayero, Houda Mouhcine
- article
- 2025
- Accès au texte intégral et bibtex
-
2013
- titre
- How to Compute the Area of a Triangle: a Formal Revisit with a Tighter Error Bound
- auteur
- Sylvie Boldo
- article
- 2013
- Accès au texte intégral et bibtex
-
2001
- titre
- Computer validated proofs of a toolset for adaptable arithmetic
- auteur
- Sylvie Boldo, Marc Daumas, Claire Moreau-Finot, Laurent Thery
- article
- 2001
- Accès au bibtex
-