BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formally Verified Approximations of Definite Integrals - Assia Mah
 boubi (INRIA Saclay - Île-de-France)
DTSTART:20170712T080000Z
DTEND:20170712T090000Z
UID:TALK73253@talks.cam.ac.uk
CONTACT:INI IT
DESCRIPTION:Co-authors: Guillaume Melquiond		(Inria\, Universit&eacute\; P
 aris-Saclay)\, Thomas Sibut-Pinote		(Inria\, Universit&eacute\; Paris-Sacl
 ay\; &Eacute\;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 o
 f the numerical integration methods can even be made rigorous: not only do
  they compute an approximation of the integral value but they also bound i
 ts inaccuracy. Yet numerical integration is still missing from the toolbox
  when performing formal proofs in analysis\, but also in other areas of ma
 thematics that shall involve the evaluation of some integrals like number 
 theory\, dynamical systems... In this talk\, we describe and discuss an ef
 ficient method for automatically computing and proving bounds on some defi
 nite integrals inside the Coq proof assistant.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR