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 metadatas

Cited literature [18 references]  Display  Hide  Download

https://hal.inria.fr/hal-00845791
Contributor : Érik Martin-Dorel <>
Submitted on : Wednesday, October 2, 2013 - 6:38:58 PM
Last modification on : Thursday, February 14, 2019 - 4:02:03 PM
Long-term archiving on : Friday, April 7, 2017 - 5:30:54 AM

File

CoqApprox2013_HAL_v2.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00845791, version 2

Collections

Citation

É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⟩

Share

Metrics

Record views

626

Files downloads

624