Bibtex Entries

@inproceedings{BroMelPio03,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {The {B}oost interval arithmetic library},
  booktitle = {Proceedings of the 5th Conference on Real Numbers and Computers},
  pages     = {65--80},
  address   = {Lyon, France},
  year      = {2003},
  hal       = {inria-00348711}
}

@inproceedings{DauMel04,
  author    = {Marc Daumas and Guillaume Melquiond},
  title     = {Generating formally certified bounds on values and round-off errors},
  booktitle = {Proceedings of the 6th Conference on Real Numbers and Computers},
  editor    = {Vasco Brattka and Christiane Frougny and Norbert M{\"u}ller},
  pages     = {55--70},
  address   = {Schlo{\ss} Dagstuhl, Germany},
  year      = {2004},
  hal       = {inria-00070739}
}

@inproceedings{DauMelMun05,
  author    = {Marc Daumas and Guillaume Melquiond and C{\'e}sar Mu{\~n}oz},
  title     = {Guaranteed proofs using interval arithmetic},
  booktitle = {Proceedings of the 17th IEEE Symposium on Computer Arithmetic},
  editor    = {Paolo Montuschi and Eric Schwarz},
  pages     = {188--195},
  address   = {Cape Cod, MA, USA},
  year      = {2005},
  doi       = {10.1109/ARITH.2005.25},
  hal       = {hal-00164621}
}

@inproceedings{BolMel05,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {When double rounding is odd},
  booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
  address   = {Paris, France},
  year      = {2005},
  hal       = {inria-00070603}
}

@inproceedings{MelPio05,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Formal certification of arithmetic filters for geometric predicates},
  booktitle = {Proceedings of the 17th IMACS World Congress on Computational and Applied Mathematics},
  address   = {Paris, France},
  year      = {2005},
  hal       = {inria-00344518}
}

@article{BroMelPio06a,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {The design of the {B}oost interval arithmetic library},
  journal   = {Theoretical Computer Science},
  editor    = {Marc Daumas and Nathalie Revol},
  pages     = {111--118},
  volume    = {351},
  year      = {2006},
  doi       = {10.1016/j.tcs.2005.09.062},
  hal       = {inria-00344412}
}

@inproceedings{DinLauMel06,
  author    = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
  title     = {Assisted verification of elementary functions using {G}appa},
  booktitle = {Proceedings of the 2006 ACM Symposium on Applied Computing},
  pages     = {1318--1322},
  address   = {Dijon, France},
  year      = {2006},
  url       = {http://www.lri.fr/~melquion/doc/06-mcms-article.pdf}
}

@techreport{BroMelPio06b,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {Bool\_set: multi-valued logic},
  institution = {ISO C++ Standardization Committee},
  number    = {2136},
  year      = {2006},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2136.pdf}
}

@techreport{BroMelPio06c,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {A Proposal to add Interval Arithmetic to the {C}++ Standard Library},
  institution = {ISO C++ Standardization Committee},
  number    = {2137},
  year      = {2006},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2006/n2137.pdf}
}

@inproceedings{BroMelPio06d,
  author    = {Herv{\'e} Br{\"o}nnimann and Guillaume Melquiond and Sylvain Pion},
  title     = {Proposing Interval Arithmetic for the {C}++ Standard},
  booktitle = {Proceedings of the 12th GAMM-IMACS International Symposium on
               Scientific Computing, Computer Arithmetic and Validated Numerics},
  address   = {Duisburg, Germany},
  year      = {2006}
}

@inproceedings{BDKM06,
  author    = {Sylvie Boldo and Marc Daumas and William Kahan and Guillaume Melquiond},
  title     = {Proof and certification for an accurate discriminant},
  booktitle = {Proceedings of the 12th GAMM-IMACS International Symposium on
               Scientific Computing, Computer Arithmetic and Validated Numerics},
  address   = {Duisburg, Germany},
  year      = {2006}
}

@phdthesis{Mel06,
  author    = {Guillaume Melquiond},
  title     = {De l'arithm{\'e}tique d'intervalles {\`a} la certification de programmes},
  school    = {\'Ecole Normale Sup\'erieure de Lyon},
  address   = {Lyon, France},
  year      = {2006},
  hal       = {tel-01094485}
}

@article{MelPio07,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Formally certified floating-point filters for homogeneous geometric predicates},
  journal   = {Theoretical Informatics and Applications},
  editor    = {Vasco Brattka and Christiane Frougny and Norbert Mueller},
  year      = {2007},
  volume    = {41},
  number    = {1},
  pages     = {57--70},
  doi       = {10.1051/ita:2007005},
  hal       = {inria-00071232}
}

@article{BolMel08,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {Emulation of a {FMA} and correctly-rounded sums: Proved algorithms using rounding to odd},
  journal   = {Transactions on Computers},
  publisher = {IEEE},
  year      = {2008},
  volume    = {57},
  number    = {4},
  pages     = {462--471},
  doi       = {10.1109/TC.2007.70819},
  hal       = {inria-00080427}
}

@inproceedings{Mel08a,
  author    = {Guillaume Melquiond},
  title     = {Floating-point arithmetic in the {C}oq system},
  booktitle = {Proceedings of the 8th Conference on Real Numbers and Computers},
  editor    = {Javier D. Bruguera and Marc Daumas},
  address   = {Santiago de Compostela, Spain},
  year      = {2008},
  month     = jul,
  pages     = {93--102},
  hal       = {hal-01780385}
}

@inproceedings{Mel08b,
  author    = {Guillaume Melquiond},
  title     = {Proving bounds on real-valued functions with computations},
  booktitle = {Proceedings of the 4th International Joint Conference on Automated Reasoning},
  editor    = {Alessandro Armando and Peter Baumgartner and Gilles Dowek},
  address   = {Sydney, Australia},
  year      = {2008},
  volume    = {5195},
  pages     = {2--17},
  series    = {Lecture Notes in Artificial Intelligence},
  doi       = {10.1007/978-3-540-71070-7_2},
  hal       = {hal-00180138}
}

@article{RZBM09,
  author    = {Siegfried M. Rump and Paul Zimmermann and Sylvie Boldo and Guillaume Melquiond},
  title     = {Computing predecessor and successor in rounding to nearest},
  journal   = {BIT Numerical Mathematics},
  year      = {2009},
  volume    = {49},
  number    = {2},
  pages     = {419--431},
  doi       = {10.1007/s10543-009-0218-z},
  hal       = {inria-00337537}
}

@inproceedings{EdmMel09,
  author    = {William Edmonson and Guillaume Melquiond},
  title     = {{IEEE} interval standard working group - {P1788}: current status},
  booktitle = {Proceedings of the 19th IEEE Symposium on Computer Arithmetic},
  editor    = {Javier D. Bruguera and Marius Cornea and Debjit DasSarma and John Harrison},
  address   = {Portland, OR, USA},
  year      = {2009},
  month     = jun,
  pages     = {231--234},
  doi       = {10.1109/ARITH.2009.36}
}

@inproceedings{BolFilMel09,
  author    = {Sylvie Boldo and Jean-Christophe Filli{\^a}tre and Guillaume Melquiond},
  title     = {Combining {C}oq and {G}appa for certifying floating-point programs},
  booktitle = {Proceedings of the 16th Calculemus Symposium},
  editor    = {Jacques Carette and Lucas Dixon and Claudio Sarcedoti Coen and Stephen M. Watt},
  year      = {2009},
  month     = jul,
  address   = {Grand Bend, ON, Canada},
  series    = {Lecture Notes in Artificial Intelligence},
  volume    = {5625},
  pages     = {59--74},
  doi       = {10.1007/978-3-642-02614-0_10},
  hal       = {inria-00432726}
}

@techreport{MelPio09,
  author    = {Guillaume Melquiond and Sylvain Pion},
  title     = {Directed rounding arithmetic operations},
  institution = {ISO C++ Standardization Committee},
  number    = {2899},
  year      = {2009},
  url       = {http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2009/n2899.pdf}
}

@article{DauMel10,
  author    = {Marc Daumas and Guillaume Melquiond},
  title     = {Certification of bounds on expressions involving rounded operators},
  journal   = {Transactions on Mathematical Software},
  publisher = {ACM},
  year      = {2010},
  volume    = {37},
  number    = {1},
  pages     = {1--20},
  doi       = {10.1145/1644001.1644003},
  hal       = {hal-00127769}
}

@book{Mul10,
  author    = {Jean-Michel Muller and Nicolas Brisebarre and Florent de Dinechin and Claude-Pierre Jeannerod and Vincent Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol and Damien Stehl{\'e} and Serge Torres},
  title     = {Handbook of Floating-Point Arithmetic},
  numpages  = {572},
  publisher = {Birkh{\"a}user},
  year      = {2010},
  doi       = {10.1007/978-0-8176-4705-6}
}

@inproceedings{BCFMMW10,
  author    = {Sylvie Boldo and François Cl{\'e}ment and Jean-Christophe Filli{\^a}tre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title     = {Formal Proof of a Wave Equation Resolution Scheme: the Method Error},
  booktitle = {Proceedings of the 1st Interactive Theorem Proving Conference},
  editor    = {Matt Kaufmann and Lawrence C. Paulson},
  year      = {2010},
  month     = jul,
  address   = {Edinburgh, Scotland, UK},
  series    = {Lecture Notes on Computer Science},
  volume    = {6172},
  pages     = {147--162},
  doi       = {10.1007/978-3-642-14052-5_12},
  hal       = {inria-00450789}
}

@article{DinLauMel11,
  author    = {Florent de Dinechin and Christoph Lauter and Guillaume Melquiond},
  title     = {Certifying the Floating-point Implementation of an Elementary Function Using {G}appa},
  journal   = {Transactions on Computers},
  volume    = {60},
  number    = {2},
  year      = {2011},
  publisher = {IEEE},
  pages     = {242--253},
  doi       = {10.1109/TC.2010.128},
  hal       = {ensl-00200830}
}

@inproceedings{BolMel11,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {Flocq: A Unified Library for Proving Floating-point Algorithms in {C}oq},
  booktitle = {Proceedings of the 20th IEEE Symposium on Computer Arithmetic},
  editor    = {Elisardo Antelo and David Hough and Paolo Ienne},
  address   = {T{\"u}bingen, Germany},
  year      = {2011},
  month     = jul,
  pages     = {243--252},
  doi       = {10.1109/ARITH.2011.40},
  hal       = {inria-00534854}
}

@inproceedings{LelMel12,
  author    = {Catherine Lelay and Guillaume Melquiond},
  title     = {Diff\'erentiabilit\'e et int\'egrabilit\'e en {C}oq. {A}pplication \`a la formule de d'{A}lembert},
  booktitle = {23\`emes Journ\'ees Francophones des Langages Applicatifs},
  year      = {2012},
  month     = feb,
  pages     = {119--133},
  address   = {Carnac, France},
  hal       = {hal-00642206}
}

@inproceedings{BCCIMMM12,
  author    = {Fran{\c c}ois Bobot and Sylvain Conchon and {\'E}velyne Contejean and Mohamed Iguernelala and Assia Mahboubi and Alain Mebsout and Guillaume Melquiond},
  title     = {A {S}implex-Based Extension of {F}ourier-{M}otzkin for Solving Linear Integer Arithmetic},
  booktitle = {Proceedings of the 6th International Joint Conference on Automated Reasoning},
  editor    = {Bernhard Gramlich and Dale Miller and Uli Sattler},
  year      = {2012},
  month     = jun,
  address   = {Manchester, UK},
  series    = {Lecture Notes in Computer Science},
  volume    = {7364},
  pages     = {67--81},
  doi       = {10.1007/978-3-642-31365-3_8},
  hal       = {hal-00687640}
}

@article{Mel12,
  author    = {Guillaume Melquiond},
  title     = {Floating-point arithmetic in the {C}oq system},
  journal   = {Information and Computation},
  volume    = {216},
  pages     = {14--23},
  year      = {2012},
  publisher = {Elsevier},
  doi       = {10.1016/j.ic.2011.09.005},
  hal       = {hal-00797913}
}

@inproceedings{CMRI12,
  author    = {Sylvain Conchon and Guillaume Melquiond and Cody Roux and Mohamed Iguernelala},
  title     = {Built-in Treatment of an Axiomatic Floating-Point Theory for {SMT} Solvers},
  booktitle = {Proceedings of the 10th International Workshop on Satisfiability Modulo Theories},
  pages     = {12--21},
  year      = {2012},
  month     = jun,
  address   = {Manchester, UK},
  hal       = {hal-01785166}
}

@inproceedings{BolLelMel12,
  author    = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title     = {Improving Real Analysis in {C}oq: a User-Friendly Approach to Integrals and Derivatives},
  booktitle = {Proceedings of the 2nd International Conference on Certified Programs and Proofs},
  editor    = {Chris Hawblitzel and Dale Miller},
  year      = {2012},
  month     = dec,
  address   = {Kyoto, Japan},
  series    = {Lecture Notes in Computer Science},
  volume    = {7679},
  pages     = {289--304},
  doi       = {10.1007/978-3-642-35308-6_22},
  hal       = {hal-00712938}
}

@article{MelNowZim13,
  author    = {Guillaume Melquiond and W. Georg Nowak and Paul Zimmermann},
  title     = {Numerical approximation of the {M}asser-{G}ramain constant to four decimal digits: $\delta = 1.819...$},
  journal   = {Mathematics of Computation},
  volume    = {82},
  pages     = {1235--1246},
  year      = {2013},
  publisher = {AMS},
  doi       = {10.1090/S0025-5718-2012-02635-4},
  hal       = {hal-00644166}
}

@article{BCFMMW13,
  author    = {Sylvie Boldo and Fran{\c c}ois Cl{\'e}ment and Jean-Christophe Filli{\^a}tre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title     = {Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a {C} Program},
  journal   = {Journal of Automated Reasoning},
  volume    = {50},
  number    = {4},
  pages     = {423--456},
  year      = {2013},
  doi       = {10.1007/s10817-012-9255-4},
  hal       = {hal-00649240}
}

@inproceedings{BJLM13,
  author    = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
  title     = {A Formally-Verified {C} Compiler Supporting Floating-Point Arithmetic},
  booktitle = {Proceedings of the 21st IEEE Symposium on Computer Arithmetic},
  editor    = {Alberto Nannarelli and Peter-Michael Seidel and Ping Tak Peter Tang},
  pages     = {107--115},
  year      = {2013},
  month     = jun,
  address   = {Austin, TX, USA},
  doi       = {10.1109/ARITH.2013.30},
  hal       = {hal-00743090}
}

@inproceedings{IshMelNak13,
  author    = {Daisuke Ishii and Guillaume Melquiond and Shin Nakajima},
  title     = {Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus},
  booktitle = {Proceedings of the 10th Conference on Integrated Formal Methods},
  editor    = {Einar Broch Johnsen and Luigia Petre},
  year      = {2013},
  month     = jun,
  address   = {Turku, Finland},
  series    = {Lecture Notes in Computer Science},
  volume    = {7940},
  pages     = {139--153},
  doi       = {10.1007/978-3-642-38613-8_10},
  hal       = {hal-00806701}
}

@article{MarMelMul13,
  author    = {{\'E}rik Martin-Dorel and Guillaume Melquiond and Jean-Michel Muller},
  title     = {Some Issues Related to Double Rounding},
  journal   = {BIT Numerical Mathematics},
  volume    = {53},
  number    = {4},
  pages     = {897--924},
  year      = {2013},
  doi       = {10.1007/s10543-013-0436-2},
  hal       = {ensl-00644408}
}

@incollection{BolMel13,
  title     = {Arithm{\'e}tique des ordinateurs et preuves formelles},
  author    = {Sylvie Boldo and Guillaume Melquiond},
  booktitle = {Informatique {M}ath{\'e}matique~: une photographie en 2013},
  editor    = {Philippe Langlois},
  pages     = {189--220},
  publisher = {Presses Universitaires de Perpignan},
  year      = {2013},
  hal       = {hal-01767900}
}

@inproceedings{BFMMP13,
  title     = {Preserving User Proofs across Specification Changes},
  author    = {Fran{\c c}ois Bobot and Jean-Christophe Filli{\^a}tre and Claude March{\'e} and Guillaume Melquiond and Andrei Paskevich},
  booktitle = {Proceedings of the 5th International Conference on Verified Software: Theories, Tools, and Experiments},
  editor    = {Ernie Cohen and Andrey Rybalchenko},
  year      = {2013},
  month     = may,
  address   = {Menlo Park, CA, USA},
  series    = {Lecture Notes in Computer Science},
  volume    = {8164},
  pages     = {191--201},
  doi       = {10.1007/978-3-642-54108-7_10},
  hal       = {hal-00875395}
}

@article{BCFMMW14,
  author    = {Sylvie Boldo and Fran{\c c}ois Cl{\'e}ment and Jean-Christophe Filli{\^a}tre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  title     = {Trusting Computations: A Mechanized Proof from Partial Differential Equations to Actual Program},
  journal   = {Computers \& Mathematics with Applications},
  volume    = {68},
  number    = {3},
  pages     = {325--352},
  year      = {2014},
  publisher = {Elsevier},
  doi       = {10.1016/j.camwa.2014.06.004},
  hal       = {hal-00769201}
}

@article{BJLM15,
  author    = {Sylvie Boldo and Jacques-Henri Jourdan and Xavier Leroy and Guillaume Melquiond},
  title     = {Verified Compilation of Floating-Point Computations},
  journal   = {Journal of Automated Reasoning},
  volume    = {54},
  number    = {2},
  pages     = {135--163},
  year      = {2015},
  doi       = {10.1007/s10817-014-9317-x},
  hal       = {hal-00862689}
}

@article{BolLelMel15,
  author    = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title     = {Coquelicot: A User-Friendly Library of Real Analysis for {C}oq},
  journal   = {Mathematics in Computer Science},
  volume    = {9},
  number    = {1},
  pages     = {41--62},
  year      = {2015},
  publisher = {Springer},
  doi       = {10.1007/s11786-014-0181-1},
  hal       = {hal-00860648}
}

@article{BolLelMel16,
  author    = {Sylvie Boldo and Catherine Lelay and Guillaume Melquiond},
  title     = {Formalization of Real Analysis: A Survey of Proof Assistants and Libraries},
  journal   = {Mathematical Structures in Computer Science},
  volume    = {26},
  number    = {7},
  pages     = {1196--1233},
  year      = {2016},
  doi       = {10.1017/S0960129514000437},
  hal       = {hal-00806920}
}

@article{MarMel16,
  author    = {{\'E}rik Martin-Dorel and Guillaume Melquiond},
  title     = {Proving Tight Bounds on Univariate Expressions with Elementary Functions in {C}oq},
  journal   = {Journal of Automated Reasoning},
  volume    = {57},
  number    = {3},
  pages     = {187--217},
  year      = {2016},
  doi       = {10.1007/s10817-015-9350-4},
  hal       = {hal-01086460}
}

@inproceedings{MahMelSib16,
  author    = {Assia Mahboubi and Guillaume Melquiond and Thomas Sibut-Pinote},
  title     = {Formally Verified Approximations of Definite Integrals},
  booktitle = {Proceedings of the 7th Conference on Interactive Theorem Proving},
  editor    = {Jasmin Christian Blanchette and Stephan Merz},
  year      = {2016},
  month     = aug,
  address   = {Nancy, France},
  series    = {Lecture Notes in Computer Science},
  volume    = {9807},
  pages     = {274--289},
  doi       = {10.1007/978-3-319-43144-4_17},
  hal       = {hal-01289616}
}

@inproceedings{CIJMF17,
  author    = {Sylvain Conchon and Mohamed Iguernlala and Kailiang Ji and Guillaume Melquiond and Cl{\'e}ment Fumex},
  title     = {A Three-tier Strategy for Reasoning about Floating-Point Numbers in {SMT}},
  booktitle = {Proceedings of the 29th International Conference on Computer Aided Verification},
  editor    = {Viktor Kuncak and Rupak Majumdar},
  year      = {2017},
  month     = jul,
  address   = {Heidelberg, Germany},
  series    = {Lecture Notes in Computer Science},
  volume    = {10427},
  pages     = {419--435},
  doi       = {10.1007/978-3-319-63390-9_22},
  hal       = {hal-01522770}
}

@inproceedings{RieMarMel17,
  author    = {Rapha{\"e}l Rieu-Helft and Claude March{\'e} and Guillaume Melquiond},
  title     = {How to Get an Efficient yet Verified Arbitrary-Precision Integer Library},
  booktitle = {Post-proceedings of the 9th Working Conference on Verified Software: Theories, Tools and Experiments},
  editor    = {Andrei Paskevich and Thomas Wies},
  year      = {2017},
  month     = jul,
  address   = {Heidelberg, Germany},
  series    = {Lecture Notes in Computer Science},
  volume    = {10712},
  pages     = {84--101},
  doi       = {10.1007/978-3-319-72308-2_6},
  hal       = {hal-01519732}
}

@book{BolMel17,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {Computer Arithmetic and Formal Proofs},
  subtitle  = {Verifying Floating-point Algorithms with the {C}oq System},
  numpages  = {326},
  publisher = {ISTE Press -- Elsevier},
  year      = {2017}
}

@book{Mul18,
  author    = {Jean-Michel Muller and Nicolas Brunie and Florent de Dinechin and Claude-Pierre Jeannerod and Mioara Joldes and Vincent Lef{\`e}vre and Guillaume Melquiond and Nathalie Revol and Serge Torres},
  title     = {Handbook of Floating-Point Arithmetic},
  numpages  = {627},
  edition   = {2},
  year      = {2018},
  publisher = {Birkh{\"a}user Basel},
  doi       = {10.1007/978-3-319-76526-6}
}

@inproceedings{MelRie18,
  author    = {Guillaume Melquiond and Rapha{\"e}l Rieu-Helft},
  title     = {A {W}hy3 Framework for Reflection Proofs and its Application to {GMP}'s Algorithms},
  booktitle = {Proceedings of the 9th International Joint Conference on Automated Reasoning},
  editor    = {Didier Galmiche and Stephan Schulz and Roberto Sebastiani},
  year      = {2018},
  month     = jul,
  address   = {Oxford, United Kingdom},
  series    = {Lecture Notes in Artificial Intelligence},
  volume    = {10900},
  pages     = {178--193},
  doi       = {10.1007/978-3-319-94205-6_13},
  hal       = {hal-01699754}
}

@article{MahMelSib19,
  author    = {Assia Mahboubi and Guillaume Melquiond and Thomas Sibut-Pinote},
  title     = {Formally Verified Approximations of Definite Integrals},
  journal   = {Journal of Automated Reasoning},
  year      = {2019},
  volume    = {62},
  number    = {2},
  pages     = {281--300},
  doi       = {10.1007/s10817-018-9463-7},
  hal       = {hal-01630143}
}

@inproceedings{MelRie19,
  author    = {Guillaume Melquiond and Rapha{\"e}l Rieu-Helft},
  title     = {Formal Verification of a State-of-the-Art Integer Square Root},
  booktitle = {Proceedings of the 26th IEEE Symposium on Computer Arithmetic},
  editor    = {Sylvie Boldo and Martin Langhammer},
  year      = {2019},
  month     = jun,
  address   = {Kyoto, Japan},
  pages     = {183--186},
  doi       = {10.1109/ARITH.2019.00041},
  hal       = {hal-02092970}
}

@phdthesis{Mel19,
  author    = {Guillaume Melquiond},
  title     = {Formal Verification for Numerical Computations, and the Other Way Around},
  type      = {Habilitation {\`a} Diriger des Recherches},
  school    = {Universit\'e Paris Sud},
  address   = {Orsay, France},
  year      = {2019},
  hal       = {tel-02194683}
}

@inproceedings{MelRie20,
  author    = {Guillaume Melquiond and Rapha{\"e}l Rieu-Helft},
  title     = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
  booktitle = {Proceedings of the 45th International Symposium on Symbolic and Algebraic Computation},
  year      = {2020},
  month     = jul,
  address   = {Kalamata, Greece},
  pages     = {352--359},
  doi       = {10.1145/3373207.3404029},
  hal       = {hal-02566654}
}

@inproceedings{Mel21,
  author    = {Guillaume Melquiond},
  title     = {Plotting in a Formally Verified Way},
  booktitle = {Proceedings of the 6th Workshop on Formal Integrated Development Environment},
  editor    = {Jos{\'e} Proen{\c c}a and Andrei Paskevich},
  year      = {2021},
  month     = may,
  series    = {Electronic Proceedings in Theoretical Computer Science},
  volume    = {338},
  pages     = {39--45},
  doi       = {10.4204/EPTCS.338.6},
  hal       = {hal-03168208}
}

@inproceedings{BolMel21,
  author    = {Sylvie Boldo and Guillaume Melquiond},
  title     = {Some Formal Tools for Computer Arithmetic: {F}locq and {G}appa},
  booktitle = {Proceedings of the 28th IEEE International Symposium on Computer Arithmetic},
  editor    = {Mioara Joldes and Fabrizio Lamberti},
  year      = {2021},
  month     = jun,
  hal       = {hal-03233227}
}

@inproceedings{BalLanMel21,
  author    = {Thibaut Balabonski and Antoine Lanco and Guillaume Melquiond},
  title     = {A Strong Call-By-Need Calculus},
  booktitle = {Proceedings of the 6th International Conference on Formal Structures for Computation and Deduction},
  editor    = {Naoki Kobayashi},
  year      = {2021},
  month     = jul,
  series    = {Leibniz International Proceedings in Informatics},
  volume    = {195},
  pages     = {9:1--9:22},
  doi       = {10.4230/LIPIcs.FSCD.2021.9},
  hal       = {hal-03149692}
}

@article{MelRie23,
  author    = {Guillaume Melquiond and Rapha{\"e}l Rieu-Helft},
  title     = {{WhyMP}, a Formally Verified Arbitrary-Precision Integer Library},
  journal   = {Journal of Symbolic Computation},
  volume    = {115},
  pages     = {74--95},
  year      = {2023},
  doi       = {10.1016/j.jsc.2022.07.007},
  hal       = {hal-03233220}
}

@article{BalLanMel23,
  author    = {Thibaut Balabonski and Antoine Lanco and Guillaume Melquiond},
  title     = {A Strong Call-By-Need Calculus},
  journal   = {Logical Methods in Computer Science},
  volume    = {19},
  number    = {1},
  pages     = {21:1--21:39},
  year      = {2023},
  month     = mar,
  doi       = {10.46298/lmcs-19(1:21)2023},
  hal       = {hal-03409681}
}

@article{BJMM23,
  author    = {Sylvie Boldo and Claude-Pierre Jeannerod and Guillaume Melquiond and Jean-Michel Muller},
  title     = {Floating-point Arithmetic},
  year      = {2023},
  journal   = {Acta Numerica},
  publisher = {Cambridge University Press},
  volume    = {32},
  pages     = {203--290},
  month     = may,
  doi       = {10.1017/S0962492922000101},
  hal       = {hal-04095151},
}

@inproceedings{MahMel23,
  author    = {Assia Mahboubi and Guillaume Melquiond},
  title     = {Manifest Termination},
  booktitle = {Proceedings of the 29th International Conference on Types for Proofs and Programs},
  editor    = {Eduardo Hermo Reyes and Alicia Villanueva},
  year      = {2023},
  month     = jun,
  address   = {Valencia, Spain},
  pages     = {172--174},
  hal       = {hal-04172297}
}

@inproceedings{GenMelFai23,
  author    = {Geneau de Lamarli{\`e}re, Paul and Guillaume Melquiond and Florian Faissole},
  title     = {Slimmer Formal Proofs for Mathematical Libraries},
  booktitle = {Proceedings of the 30th IEEE International Symposium on Computer Arithmetic},
  editor    = {Theo Drane and Anastasia Volkova},
  year      = {2023},
  month     = sep,
  address   = {Portland, OR, USA},
  hal       = {hal-04165169}
}

@article{MarMelRou23,
  author    = {{\'E}rik Martin-Dorel and Guillaume Melquiond and Pierre Roux},
  title     = {Enabling Floating-Point Arithmetic in the {C}oq Proof Assistant},
  year      = {2023},
  journal   = {Journal of Automated Reasoning},
  volume    = {67},
  doi       = {10.1007/s10817-023-09679-x},
  hal       = {hal-04114233}
}

@inproceedings{MelMor24,
  author    = {Josu{\`e} Moreau and Guillaume Melquiond},
  title     = {A Safe Low-level Language for Computer Algebra and its Formally Verified Compiler},
  booktitle = {Proceedings of the 29th ACM SIGPLAN International Conference on Functional Programming},
  editor    = {Brigitte Pientka},
  year      = {2024},
  month     = sep,
  address   = {Milan, Italy},
  series    = {Proceedings of the ACM on Programming Languages}
  volume    = {8},
  number    = {ICFP},
  pages     = {121--146},
  doi       = {10.1145/3674629},
  hal       = {hal-04485670}
}

@inproceedings{FaiGenMel24,
  author    = {Florian Faissole and Geneau de Lamarli{\`e}re, Paul and Guillaume Melquiond},
  title     = {End-to-End Formal Verification of a Fast and Accurate Floating-Point Approximation},
  booktitle = {Proceedings of the 15th International Conference on Interactive Theorem Proving},
  editor    = {Yves Bertot and Temur Kutsia and Michael Norrish},
  year      = {2024},
  month     = sep,
  address   = {Tbilisi, Georgia},
  series    = {Leibniz International Proceedings in Informatics},
  volume    = {309},
  pages     = {14:1--14:18},
  doi       = {10.4230/LIPIcs.ITP.2024.14},
  hal       = {hal-04515714}
}

@inproceedings{Mel24,
  author    = {Guillaume Melquiond},
  title     = {Turning the {C}oq Proof Assistant into a Pocket Calculator},
  booktitle = {Proceedings of the 15th Coq Workshop},
  editor    = {Cl{\'e}ment Piet-Claudel and Th{\'e}o Winterhalter},
  year      = {2024},
  month     = sep,
  address   = {Tbilisi, Georgia},
  hal       = {hal-04702129}
}