Proving tight bounds on univariate expressions with elementary functions in Coq
From MaRDI portal
Publication:331615
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
interval arithmeticfloating-point arithmeticformal proofdecision procedurenonlinear arithmeticCoq proof assistant
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (7)
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
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
This page was built for publication: Proving tight bounds on univariate expressions with elementary functions in Coq
