Proving tight bounds on univariate expressions with elementary functions in Coq

DOI10.1007/s10817-015-9350-4zbMath1386.68151OpenAlexW1915348541MaRDI QIDQ331615

Guillaume Melquiond, Érik Martin-Dorel

Publication date: 27 October 2016

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-01086460/file/article.pdf

zbMATH Keywords

interval arithmeticfloating-point arithmeticformal proofdecision procedurenonlinear arithmeticCoq proof assistant

Mathematics Subject Classification ID

Roundoff error (65G50) Series expansions (e.g., Taylor, Lidstone series, but not Fourier series) (41A58)

Related Items

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem, Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation, A verified ODE solver and the Lorenz attractor, Enabling floating-point arithmetic in the Coq proof assistant, Formally verified approximations of definite integrals, A certificate-based approach to formally verified approximations, Primitive Floats in Coq

Uses Software

• Coq
• MetiTarski
• PVS
• Flocq
• Sollya

Cites Work

• Unnamed Item
• Unnamed Item
• Efficient and accurate computation of upper bounds of approximation errors
• Floating-point arithmetic in the Coq system
• MetiTarski: An automatic theorem prover for real-valued special functions
• Horner's rule for interval evaluation revisited
• Formalization of Bernstein polynomials and applications to global optimization
• Certification of Bounds of Non-linear Functions: The Templates Method
• Verifying Nonlinear Real Formulas Via Sums of Squares
• Proving Bounds on Real-Valued Functions with Computations
• Handbook of Floating-Point Arithmetic
• Table-driven implementation of the exponential function in IEEE floating-point arithmetic
• Fast evaluation of elementary mathematical functions with correctly rounded last bit
• Verified Real Number Calculations: A Library for Interval Arithmetic
• Sollya: An Environment for the Development of Numerical Codes