On Monday 26/08/2013, at 14h30, in room Byron Blanc.
Speaker: Érik Martin-Dorel.
Title: Certified, Efficient and Sharp Univariate Taylor Models in COQ.
Abstract:
We present a formalisation, within the COQ proof assistant, of
univariate Taylor models. This formalisation being executable, we get a
generic library whose correctness has been formally proved and with
which one can effectively compute rigorous and sharp approximations of
univariate functions composed of usual functions such as 1/x, sqrt(x),
exp(x), sin(x) among others. In this talk, we present the key parts of
the formalisation and we evaluate the quality of our certified library
on a set of examples.
- Joint work with members of the CoqApprox working group
http://tamadi.gforge.inria.fr/CoqApprox - URL of the paper: HAL page
