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

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Guillaume Melquiond