Skip to Main content Skip to Navigation
Conference papers

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 paper, we present the key parts of the formalisation and we evaluate the quality of our certified library on a set of examples.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Érik Martin-Dorel Connect in order to contact the contributor
Submitted on : Wednesday, October 2, 2013 - 6:38:58 PM
Last modification on : Tuesday, November 23, 2021 - 3:46:48 AM
Long-term archiving on: : Friday, April 7, 2017 - 5:30:54 AM


Files produced by the author(s)


  • HAL Id : hal-00845791, version 2


Érik Martin-Dorel, Micaela Mayero, Ioana Pasca, Laurence Rideau, Laurent Théry. Certified, Efficient and Sharp Univariate Taylor Models in COQ. SYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania. ⟨hal-00845791v2⟩



Les métriques sont temporairement indisponibles