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.
Type de document :
Communication dans un congrès
SYNASC 2013 - 15th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, Sep 2013, Timisoara, Romania. 2013
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00845791
Contributeur : Érik Martin-Dorel <>
Soumis le : mercredi 2 octobre 2013 - 18:38:58
Dernière modification le : jeudi 11 janvier 2018 - 16:49:58
Document(s) archivé(s) le : vendredi 7 avril 2017 - 05:30:54

Fichier

CoqApprox2013_HAL_v2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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. 2013. 〈hal-00845791v2〉

Partager

Métriques

Consultations de la notice

573

Téléchargements de fichiers

504