Rigorous Polynomial Approximation using Taylor Models in Coq

Nicolas Brisebarre 1, 2 Mioara Maria Joldes 3 Érik Martin-Dorel 1, 2 Micaela Mayero 1, 4 Jean-Michel Muller 1, 2 Ioana Pasca 1 Laurence Rideau 5 Laurent Théry 5
1 ARENAIRE - Computer arithmetic
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
2 ARIC - Arithmetic and Computing
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 Department of Mathematics [Uppsala]
4 LIPN - Laboratoire d'Informatique de Paris-Nord
5 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : One of the most common and practical ways of representing a real function on machines is by using a polynomial approximation. It is then important to properly handle the error introduced by such an approximation. The purpose of this work is to offer guaranteed error bounds for a specific kind of rigorous polynomial approximation called Taylor model. We carry out this work in the Coq proof assistant, with a special focus on genericity and efficiency for our implementation. We give an abstract interface for rigorous polynomial approximations, parameter- ized by the type of coefficients and the implementation of polynomials, and we instantiate this interface to the case of Taylor models with inter- val coefficients, while providing all the machinery for computing them. We compare the performances of our implementation in Coq with those of the Sollya tool, which contains an implementation of Taylor models written in C. This is a milestone in our long-term goal of providing fully formally proved and efficient Taylor models.
Keywords : certified error bounds Taylor models Coq proof assistant rigorous polynomial approximation
Type de document :
Communication dans un congrès
Alwyn Goodloe and Suzette Person. Fourth NASA Formal Methods Symposium, Apr 2012, Norfolk, Virginia, United States. Springer, pp.15, 2012, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [40 références]  Voir  Masquer  Télécharger
https://hal-ens-lyon.archives-ouvertes.fr/ensl-00653460
Contributeur : Jean-Michel Muller <>
Soumis le : vendredi 6 avril 2012 - 08:48:39
Dernière modification le : vendredi 20 avril 2018 - 15:44:26
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 20:34:33

Fichier

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

Identifiants

  • HAL Id : ensl-00653460, version 2

Collections

ENS-LYON | INRIA | LIP | UNIV-PARIS13 | LIPN | USPC | UNIV-COTEDAZUR | UNIV-LYON1

Citation

Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, et al.. Rigorous Polynomial Approximation using Taylor Models in Coq. Alwyn Goodloe and Suzette Person. Fourth NASA Formal Methods Symposium, Apr 2012, Norfolk, Virginia, United States. Springer, pp.15, 2012, Lecture Notes in Computer Science. 〈ensl-00653460v2〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

1138

Téléchargements de fichiers

334

Contact

support.ccsd.cnrs.fr
hal.support@ccsd.cnrs.fr
Logo CCSD