Certified, Efficient and Sharp Univariate Taylor Models in COQ

We present a library for univariate Taylor models that has been developed with the COQ proof assistant. Each algorithm of this library is executable and has been formally proved correct. Using this library, one can then effectively compute rigorous and sharp approximations of univariate functions composed of usual functions such as reciprocal, square root, exponential, or sine among others. In this paper, we present the key parts of the formalisation as well as of the proofs of correctness, and we evaluate the quality of our certified library on a set of examples.