Formally Verified Approximations of Definite Integrals
DOI10.1007/978-3-319-43144-4_17zbMATH Open1468.68300OpenAlexW2304289376MaRDI QIDQ2829263FDOQ2829263
Thomas Sibut-Pinote, Guillaume Melquiond, Assia Mahboubi
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
Numerical integration (65D30) Interval and finite arithmetic (65G30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Cites Work
- Title not available (Why is that?)
- Coquelicot: a user-friendly library of real analysis for Coq
- Introduction to Interval Analysis
- 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 (7)
- 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
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)
