Formally Verified Approximations of Definite Integrals

Add to your list(s) Download to your calendar using vCal

• Assia Mahboubi (INRIA Saclay - Île-de-France)
• Wednesday 12 July 2017, 09:00-10:00
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact INI IT.

BPRW01 - Computer-aided mathematical proof

Co-authors: Guillaume Melquiond (Inria, Université Paris-Saclay), Thomas Sibut-Pinote (Inria, Université Paris-Saclay; École polytechnique) Finding an elementary form for an antiderivative is often a difficult task, thus numerical integration is a common tool when it comes to making sense of a definite integral. Some of the numerical integration methods can even be made rigorous: not only do they compute an approximation of the integral value but they also bound its inaccuracy. Yet numerical integration is still missing from the toolbox when performing formal proofs in analysis, but also in other areas of mathematics that shall involve the evaluation of some integrals like number theory, dynamical systems… In this talk, we describe and discuss an efficient method for automatically computing and proving bounds on some definite integrals inside the Coq proof assistant.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.