Guillaume Melquiond

Available identifiers

zbMath Open melquiond.guillaumeMaRDI QIDQ331614

List of research outcomes

Publication	Date of Publication	Type
Enabling floating-point arithmetic in the Coq proof assistant	2023-10-24	Paper
Floating-point arithmetic	2023-09-12	Paper
A strong call-by-need calculus	2023-08-26	Paper
A strong call-by-need calculus	2023-06-23	Paper
WhyMP, a formally verified arbitrary-precision integer library	2022-09-22	Paper
A three-tier strategy for reasoning about floating-point numbers in SMT	2022-08-12	Paper
WhyMP, a formally verified arbitrary-precision integer library	2021-01-22	Paper
Formally verified approximations of definite integrals	2019-02-18	Paper
How to get an efficient yet verified arbitrary-precision integer library	2018-12-07	Paper
A Why3 framework for reflection proofs and its application to GMP's algorithms	2018-10-18	Paper
Handbook of Floating-Point Arithmetic	2018-04-04	Paper
Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd	2017-11-10	Paper
Trusting computations: a mechanized proof from partial differential equations to actual program	2017-08-21	Paper
Certifying the Floating-Point Implementation of an Elementary Function Using Gappa	2017-07-27	Paper
https://portal.mardi4nfdi.de/entity/Q5274886	2017-07-06	Paper
Certification of bounds on expressions involving rounded operators	2017-05-19	Paper
Formalization of real analysis: a survey of proof assistants and libraries	2017-04-03	Paper
Proving tight bounds on univariate expressions with elementary functions in Coq	2016-10-27	Paper
Formally Verified Approximations of Definite Integrals	2016-10-27	Paper
Verified compilation of floating-point computations	2015-07-02	Paper
Coquelicot: a user-friendly library of real analysis for Coq	2015-03-25	Paper
Some issues related to double rounding	2014-02-03	Paper
Wave equation numerical resolution: a comprehensive mechanized proof of a C program	2013-07-05	Paper
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives	2013-04-19	Paper
Numerical approximation of The Masser-Gramain constant to four decimal digits: $\delta = 1.819...$	2013-03-20	Paper
Floating-point arithmetic in the Coq system	2012-10-11	Paper
A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic	2012-09-05	Paper
Formal Proof of a Wave Equation Resolution Scheme: The Method Error	2010-09-14	Paper
Computing predecessor and successor in rounding to nearest	2009-07-24	Paper
Combining Coq and Gappa for Certifying Floating-Point Programs	2009-07-09	Paper
Handbook of Floating-Point Arithmetic	2009-05-26	Paper
Proving Bounds on Real-Valued Functions with Computations	2008-11-27	Paper
Formally certified floating-point filters for homogeneous geometric predicates	2008-02-22	Paper
The design of the Boost interval arithmetic library	2006-03-20	Paper

Research outcomes over time

This page was built for person: Guillaume Melquiond