The following pages link to Guillaume Melquiond (Q331614):
Displayed 33 items.
- Proving tight bounds on univariate expressions with elementary functions in Coq (Q331615) (← links)
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program (Q352952) (← links)
- Floating-point arithmetic in the Coq system (Q714617) (← links)
- The design of the Boost interval arithmetic library (Q817867) (← links)
- How to get an efficient yet verified arbitrary-precision integer library (Q1630031) (← links)
- Formally verified approximations of definite integrals (Q1722649) (← links)
- A Why3 framework for reflection proofs and its application to GMP's algorithms (Q1799078) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- A three-tier strategy for reasoning about floating-point numbers in SMT (Q2164244) (← links)
- Verified compilation of floating-point computations (Q2352505) (← links)
- Computing predecessor and successor in rounding to nearest (Q2391021) (← links)
- Trusting computations: a mechanized proof from partial differential equations to actual program (Q2398899) (← links)
- Some issues related to double rounding (Q2434938) (← links)
- WhyMP, a formally verified arbitrary-precision integer library (Q2673999) (← links)
- Formally Verified Approximations of Definite Integrals (Q2829263) (← links)
- A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic (Q2908479) (← links)
- Formalization of real analysis: a survey of proof assistants and libraries (Q2973239) (← links)
- Certification of bounds on expressions involving rounded operators (Q2989081) (← links)
- Proving Bounds on Real-Valued Functions with Computations (Q3541683) (← links)
- Handbook of Floating-Point Arithmetic (Q3629031) (← links)
- Combining Coq and Gappa for Certifying Floating-Point Programs (Q3637269) (← links)
- Emulation of a FMA and Correctly Rounded Sums: Proved Algorithms Using Rounding to Odd (Q4589559) (← links)
- Handbook of Floating-Point Arithmetic (Q4609588) (← links)
- Numerical approximation of The Masser-Gramain constant to four decimal digits: $\delta = 1.819...$ (Q4912025) (← links)
- Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives (Q4916067) (← links)
- WhyMP, a formally verified arbitrary-precision integer library (Q5145995) (← links)
- (Q5274886) (← links)
- Certifying the Floating-Point Implementation of an Elementary Function Using Gappa (Q5280635) (← links)
- Formally certified floating-point filters for homogeneous geometric predicates (Q5444102) (← links)
- Formal Proof of a Wave Equation Resolution Scheme: The Method Error (Q5747647) (← links)
- Floating-point arithmetic (Q6047500) (← links)
- Enabling floating-point arithmetic in the Coq proof assistant (Q6053846) (← links)
- A strong call-by-need calculus (Q6135746) (← links)