Certified, Efficient and Sharp Univariate Taylor Models in COQ - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2013

Certified, Efficient and Sharp Univariate Taylor Models in COQ

Résumé

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
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

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

Identifiants

  • HAL Id : hal-00845791 , version 2

Citer

É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⟩
398 Consultations
1045 Téléchargements

Partager

Gmail Facebook X LinkedIn More