Formally Verified Approximations of Definite Integrals

DOI10.1007/978-3-319-43144-4_17zbMath1468.68300OpenAlexW2304289376MaRDI QIDQ2829263

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

Mathematics Subject Classification ID

Interval and finite arithmetic (65G30) Numerical integration (65D30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

A verified ODE solver and the Lorenz attractor ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Formally verified approximations of definite integrals ⋮ Extensional constructive real analysis via locators

Uses Software

• Coq
• Octave
• INTLAB
• Coquelicot

Cites Work

• A computer-verified monadic functional implementation of the integral
• Double bubbles minimize
• Coquelicot: a user-friendly library of real analysis for Coq
• Formally verified certificate checkers for hardest-to-round computation
• Verification methods: Rigorous results using floating-point arithmetic
• Introduction to Interval Analysis
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Unnamed Item

This page was built for publication: Formally Verified Approximations of Definite Integrals