Reseña: “Certified, efficient and sharp univariate Taylor models in Coq”
Se ha publicado un artículo de razonamiento formalizado en Coq titulado Certified, efficient and sharp univariate Taylor models in Coq.
Sus autores son
- Érik Martin-Dorel (del Inria Sophia Antipolis),
- Laurence Rideau (del Inria Sophia Antipolis),
- Laurent Théry (del Inria Sophia Antipolis),
- Micaela Mayero (de la Université Paris 13) y
- Ioana Paşca (de la Université Montpellier 2).
Su resumen es
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 paper, we present the key parts of the formalisation and we evaluate the quality of our certified library on a set of examples.