Guaranteed Proofs Using Interval Arithmetic. - Marc Daumas; Guillaume Melquiond; César A. Muñoz (IEEE Symposium on Computer Arithmetic, 2005)

A Proposal to add Interval Arithmetic to the C++ Standard Library. - Sylvain Pion; Hervé Brönnimann; Guillaume Melquiond (Reliable Implementation of Real Number Algorithms, 2006)

Assisted verification of elementary functions using Gappa. - Florent de Dinechin; Christoph Quirin Lauter; Guillaume Melquiond (SAC, 2006)

The design of the Boost interval arithmetic library. - Hervé Brönnimann; Guillaume Melquiond; Sylvain Pion (Theor. Comput. Sci., 2006)

De l'arithmétique d'intervalles à la certification de programmes. (From interval arithmetic to program verification). - Guillaume Melquiond (2006)

Formally certified floating-point filters for homogeneous geometric predicates. - Guillaume Melquiond; Sylvain Pion (RAIRO Theor. Informatics Appl., 2007)

Proving Bounds on Real-Valued Functions with Computations. - Guillaume Melquiond (IJCAR, 2008)

Certifying floating-point implementations using Gappa - Florent de Dinechin; Christoph Quirin Lauter; Guillaume Melquiond (CoRR, 2008)

Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd. - Sylvie Boldo; Guillaume Melquiond (IEEE Trans. Computers, 2008)

IEEE Interval Standard Working Group - P1788: Current Status. - William W. Edmonson; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2009)

Combining Coq and Gappa for Certifying Floating-Point Programs. - Sylvie Boldo; Jean-Christophe Filliâtre; Guillaume Melquiond (Calculemus/MKM, 2009)

Handbook of Floating-Point Arithmetic. - Jean-Michel Muller; Nicolas Brisebarre; Florent de Dinechin; Claude-Pierre Jeannerod; Vincent Lefèvre; Guillaume Melquiond; Nathalie Revol; Damien Stehlé; Serge Torres (Birkhäuser, 2010)

Formal Proof of a Wave Equation Resolution Scheme: The Method Error. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (ITP, 2010)

Certification of bounds on expressions involving rounded operators. - Marc Daumas; Guillaume Melquiond (ACM Trans. Math. Softw., 2010)

Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. - Sylvie Boldo; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2011)

Wave Equation Numerical Resolution: Mathematics and Program - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (CoRR, 2011)

Certifying the Floating-Point Implementation of an Elementary Function Using Gappa. - Florent de Dinechin; Christoph Quirin Lauter; Guillaume Melquiond (IEEE Trans. Computers, 2011)

A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. - François Bobot; Sylvain Conchon; Evelyne Contejean; Mohamed Iguernelala; Assia Mahboubi; Alain Mebsout; Guillaume Melquiond (IJCAR, 2012)

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers. - Sylvain Conchon; Guillaume Melquiond; Cody Roux; Mohamed Iguernelala (SMT@IJCAR, 2012)

Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (CPP, 2012)

Floating-point arithmetic in the Coq system. - Guillaume Melquiond (Inf. Comput., 2012)

A Formally-Verified C Compiler Supporting Floating-Point Arithmetic. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (IEEE Symposium on Computer Arithmetic, 2013)

Inductive Verification of Hybrid Automata with Strongest Postcondition Calculus. - Daisuke Ishii; Guillaume Melquiond; Shin Nakajima 001 (IFM, 2013)

Preserving User Proofs across Specification Changes. - François Bobot; Jean-Christophe Filliâtre; Claude Marché; Guillaume Melquiond; Andrei Paskevich (VSTTE, 2013)

Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (J. Autom. Reason., 2013)

Numerical approximation of The Masser-Gramain constant to four decimal digits: δ = 1.819.... - Guillaume Melquiond; W. Georg Nowak; Paul Zimmermann (Math. Comput., 2013)

Automating the Verification of Floating-Point Algorithms. - Guillaume Melquiond (SMT, 2014)

Trusting computations: A mechanized proof from partial differential equations to actual program. - Sylvie Boldo; François Clément; Jean-Christophe Filliâtre; Micaela Mayero; Guillaume Melquiond; Pierre Weis (Comput. Math. Appl., 2014)

Verified Compilation of Floating-Point Computations. - Sylvie Boldo; Jacques-Henri Jourdan; Xavier Leroy; Guillaume Melquiond (J. Autom. Reason., 2015)

Coquelicot: A User-Friendly Library of Real Analysis for Coq. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Comput. Sci., 2015)

Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. - Érik Martin-Dorel; Guillaume Melquiond (J. Autom. Reason., 2016)

Formalization of real analysis: a survey of proof assistants and libraries. - Sylvie Boldo; Catherine Lelay; Guillaume Melquiond (Math. Struct. Comput. Sci., 2016)

Computer Arithmetic and Formal Proofs - Verifying Floating-point Algorithms with the Coq System. - Sylvie Boldo; Guillaume Melquiond (ISTE Press, 2017)

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT. - Sylvain Conchon; Mohamed Iguernelala; Kailiang Ji; Guillaume Melquiond; Clément Fumex (CAV (2), 2017)

How to Get an Efficient yet Verified Arbitrary-Precision Integer Library. - Raphaël Rieu-Helft; Claude Marché; Guillaume Melquiond (VSTTE, 2017)

Handbook of Floating-Point Arithmetic (2nd Ed.). - Jean-Michel Muller; Nicolas Brunie; Florent de Dinechin; Claude-Pierre Jeannerod; Mioara Joldes; Vincent Lefèvre; Guillaume Melquiond; Nathalie Revol; Serge Torres (Springer, 2018)

A Why3 Framework for Reflection Proofs and Its Application to GMP's Algorithms. - Guillaume Melquiond; Raphaël Rieu-Helft (IJCAR, 2018)

Formal Verification for Numerical Computations, and the Other Way Around. - Guillaume Melquiond (2019)

Formal Verification of a State-of-the-Art Integer Square Root. - Guillaume Melquiond; Raphaël Rieu-Helft (ARITH, 2019)

Formally Verified Approximations of Definite Integrals. - Assia Mahboubi; Guillaume Melquiond; Thomas Sibut-Pinote (J. Autom. Reason., 2019)

Some Formal Tools for Computer Arithmetic: Flocq and Gappa. - Sylvie Boldo; Guillaume Melquiond (ARITH, 2021)

Plotting in a Formally Verified Way. - Guillaume Melquiond (F-IDE@NFM, 2021)

Slimmer Formal Proofs for Mathematical Libraries. - Paul Geneau de Lamarlière; Guillaume Melquiond; Florian Faissole (ARITH, 2023)

WhyMP, a formally verified arbitrary-precision integer library. - Guillaume Melquiond; Raphaël Rieu-Helft (J. Symb. Comput., 2023)

A strong call-by-need calculus. - Thibaut Balabonski; Antoine Lanco; Guillaume Melquiond (Log. Methods Comput. Sci., 2023)

Floating-point arithmetic. - Sylvie Boldo; Claude-Pierre Jeannerod; Guillaume Melquiond; Jean-Michel Muller (Acta Numer., 2023)

Enabling Floating-Point Arithmetic in the Coq Proof Assistant. - Érik Martin-Dorel; Guillaume Melquiond; Pierre Roux 001 (J. Autom. Reason., 2023)

End-To-End Formal Verification of a Fast and Accurate Floating-Point Approximation. - Florian Faissole; Paul Geneau de Lamarlière; Guillaume Melquiond (ITP, 2024)

A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. - Guillaume Melquiond; Josué Moreau (Proc. ACM Program. Lang., 2024)

CoqInterval. - Paul Geneau de Lamarlière; Guillaume Melquiond (DROPS Artifacts, 2024)