Certified, Efficient and Sharp Univariate Taylor Models in COQ - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

Certified, Efficient and Sharp Univariate Taylor Models in COQ

(1) , (2) , (3) , (1) , (1)
1
2
3

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.
Fichier principal
Vignette du fichier
CoqApprox2013_HAL_v2.pdf (620.98 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00845791 , version 1 (17-07-2013)
hal-00845791 , version 2 (02-10-2013)

Identifiers

  • HAL Id : hal-00845791 , version 2

Cite

É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⟩
381 View
968 Download

Share

Gmail Facebook Twitter LinkedIn More