Publications HAL

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
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
https://hal.science/hal-04095151/file/floatingpoint_arithmetic.pdf 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
https://inria.hal.science/hal-03471095/file/article.pdf 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
https://inria.hal.science/hal-03329933/file/article.pdf 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
https://hal.science/hal-02137968/file/Emulation-RN0-revised.pdf 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
https://inria.hal.science/hal-01939097/file/main.pdf 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
https://hal.science/hal-01883843/file/hal_article.pdf 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
https://ens-lyon.hal.science/ensl-01310023/file/FaithfulTwoSum-Final-Fev2017.pdf 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
https://inria.hal.science/hal-00806920/file/article.pdf 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
https://inria.hal.science/hal-00862689/file/floating-point-compcert.pdf 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
https://inria.hal.science/hal-00860648/file/article.pdf 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
https://inria.hal.science/hal-00769201/file/RR-8197.pdf 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
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
https://inria.hal.science/hal-00649240/file/RR-7826.pdf 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
https://inria.hal.science/hal-00777605/file/boldo11mcs.pdf 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
https://inria.hal.science/hal-00777639/file/ISSE.pdf 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
https://inria.hal.science/inria-00429617/file/fma_err.pdf BibTex

2010

titre
Un algorithme de découpe de gâteau
auteur
Sylvie Boldo
article
Interstices, 2010
Accès au bibtex
BibTex
titre
C'est la faute à l'ordinateur !
auteur
Sylvie Boldo
article
Interstices, 2010
Accès au bibtex
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
https://hal.science/hal-00168401/file/BDL.pdf BibTex
titre
Demandez le programme
auteur
Sylvie Boldo
article
Interstices, 2009
Accès au bibtex
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
https://inria.hal.science/inria-00171497/file/boldo.pdf 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
https://inria.hal.science/inria-00337537/file/RuZiBoMe08.pdf 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
BibTex

2008

titre
Pourquoi mon ordinateur calcule-t-il faux ?
auteur
Sylvie Boldo, Joanna Jongwane
article
Interstices, 2008
Accès au bibtex
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
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
https://ens-lyon.hal.science/inria-00080427/file/odd-rounding.pdf 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
https://inria.hal.science/inria-00071879/file/RR-4707.pdf 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
https://hal.science/hal-00157268/file/BolDau04a.pdf 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
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
https://hal.science/hal-04725586/file/article.pdf 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
https://inria.hal.science/hal-03889276/file/article.pdf 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
https://inria.hal.science/hal-03233227/file/article.pdf 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
https://inria.hal.science/hal-02982017/file/paper_17.pdf 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
https://inria.hal.science/hal-01772272/file/article-HAL.pdf 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
https://inria.hal.science/hal-01728828/file/CICM18.pdf 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
https://inria.hal.science/hal-01391578/file/article.pdf 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
https://hal.science/hal-01512417/file/itp17.pdf 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
https://hal.science/hal-01581807/file/article_afadl.pdf 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
https://hal.science/hal-01581794/file/arith_hal.pdf 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
https://inria.hal.science/hal-01377155/file/abstract.pdf 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
https://inria.hal.science/hal-01377152/file/article.pdf 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
https://inria.hal.science/hal-01148409/file/article.pdf 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
https://inria.hal.science/hal-01174892/file/article.pdf 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
https://inria.hal.science/hal-01088692/file/article.pdf 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
https://inria.hal.science/hal-00743090/file/article.pdf 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
https://inria.hal.science/hal-00790071/file/article.pdf 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
https://inria.hal.science/hal-00712938/file/article.pdf 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
https://inria.hal.science/hal-00755333/file/main.pdf 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
https://inria.hal.science/inria-00534854/file/11-arith20-article.pdf 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
https://inria.hal.science/inria-00534400/file/article.pdf 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
https://inria.hal.science/inria-00450789/file/RR-7181.pdf 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
https://inria.hal.science/inria-00534410/file/index.pdf 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
https://inria.hal.science/inria-00432726/file/09-calculemus-article.pdf 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
https://hal.science/hal-00135090/file/rnc.pdf 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
https://inria.hal.science/inria-00000892/file/main.pdf 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
https://inria.hal.science/inria-00000895/file/ARITH17_Boldo.pdf 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
https://inria.hal.science/inria-00070603/file/BolMel.pdf 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
https://hal.science/hal-00156244/file/LiBolDau03.pdf 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
https://inria.hal.science/inria-00072115/file/RR-4473.pdf 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
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
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
https://inria.hal.science/tel-01089643/file/hdr.pdf 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
BibTex

2010

titre
L'informatique
auteur
Sylvie Boldo
article
2010
Accès au bibtex
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
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
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
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
https://inria.hal.science/inria-00536135/file/posterDIGITEO.pdf 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
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
https://inria.hal.science/hal-01707376/file/jfla2018.pdf 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
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
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
https://hal.science/hal-05539615/file/Code_de_Conduite.pdf 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
https://inria.hal.science/hal-05396759/file/RR-9604.pdf 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
https://inria.hal.science/hal-05128905/file/RR-9590.pdf 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
https://inria.hal.science/hal-04550762/file/RR-9547.pdf 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
https://inria.hal.science/hal-03564379/file/RR-9457.pdf 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
https://inria.hal.science/hal-03516749/file/RR-9456.pdf 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
https://inria.hal.science/hal-03194113/file/RR-9401.pdf 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
https://inria.hal.science/hal-00804915/file/Mediation-scientifique-v0.2.pdf 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
https://hal-lara.archives-ouvertes.fr/hal-02101859/file/RR2004-41.pdf 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
https://hal-lara.archives-ouvertes.fr/hal-02101979/file/RR2004-48.pdf 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
https://hal-lara.archives-ouvertes.fr/hal-02102015/file/RR2003-01.pdf 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
https://inria.hal.science/inria-00071941/file/RR-4644.pdf 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
https://inria.hal.science/hal-05396788/file/article.pdf 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
https://inria.hal.science/hal-05128954/file/article.pdf 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
https://inria.hal.science/hal-00862653/file/article.pdf 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
https://arxiv.org/pdf/cs.MS/0107025 BibTex