Tag: proof assistant

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