Formally verified approximations of definite integrals
DOI10.1007/978-3-319-43144-4_17zbMATH Open1468.68300OpenAlexW2304289376MaRDI QIDQ2829263FDOQ2829263
Authors: Assia Mahboubi, Guillaume Melquiond, Thomas Sibut-Pinote 
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01289616v2/file/main.pdf
Recommendations
- Formally verified approximations of definite integrals
- Proving tight bounds on univariate expressions with elementary functions in Coq
- Proving Bounds on Real-Valued Functions with Computations
- scientific article; zbMATH DE number 1927426
- An adaptive numerical integration algorithm with automatic result verification for definite integrals
Numerical integration (65D30) Interval and finite arithmetic (65G30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Coquelicot: a user-friendly library of real analysis for Coq
- Introduction to Interval Analysis
- Validated numerics. A short introduction to rigorous computations.
- Verification methods: rigorous results using floating-point arithmetic
- A computer-verified monadic functional implementation of the integral
- Double bubbles minimize
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Formally verified certificate checkers for hardest-to-round computation
Cited In (8)
- Formally-verified round-off error analysis of Runge-Kutta methods
- Extensional constructive real analysis via locators
- Formally verified approximations of definite integrals
- A verified ODE solver and the Lorenz attractor
- Verified interactive computation of definite integrals
- Two adaptive Gauss-Legendre type algorithms for the verified computation of definite integrals
- Principles of verified numerical integration
- Proving Bounds on Real-Valued Functions with Computations
Uses Software
This page was built for publication: Formally verified approximations of definite integrals
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829263)
