Rigorous Polynomial Approximation using 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 : 2012

Rigorous Polynomial Approximation using Taylor Models in Coq

Mioara Maria Joldes
Ioana Pasca
  • Fonction : Auteur
  • PersonId : 845903
Laurence Rideau
  • Fonction : Auteur
  • PersonId : 832430
Laurent Théry

Résumé

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.
Fichier principal
Vignette du fichier
NFM2012_Brisebarre_et_al.pdf (503.04 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

ensl-00653460 , version 1 (19-12-2011)
ensl-00653460 , version 2 (06-04-2012)

Identifiants

  • HAL Id : ensl-00653460 , version 2

Citer

Nicolas Brisebarre, Mioara Maria Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, et al.. Rigorous Polynomial Approximation using Taylor Models in Coq. Fourth NASA Formal Methods Symposium, NASA, Apr 2012, Norfolk, Virginia, United States. pp.15. ⟨ensl-00653460v2⟩
841 Consultations
870 Téléchargements

Partager

Gmail Facebook X LinkedIn More