A New Formalization of Power Series in Coq

Catherine Lelay 1, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
Résumé : Les fonctions élémentaires sont habituellement définies dans les assistants de preuve en utilisant des séries entières. Celle qui sont formalisées dans la bibliothèque standard de Coq sont malheureusement peu développées. Cet article présente une nouvelle formalisation basée sur des limites définies comme des fonctions totales. Mon cas d'étude sont les fonctions de Bessel.
Type de document :
Communication dans un congrès
The 5th Coq Workshop, Jul 2013, Rennes, France. 2013, <http://coq.inria.fr/coq-workshop/2013>
Liste complète des métadonnées


https://hal.inria.fr/hal-00880212
Contributeur : Catherine Lelay <>
Soumis le : mardi 5 novembre 2013 - 15:49:26
Dernière modification le : jeudi 9 février 2017 - 15:00:50
Document(s) archivé(s) le : vendredi 7 avril 2017 - 21:45:14

Fichier

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

Identifiants

  • HAL Id : hal-00880212, version 1

Citation

Catherine Lelay. A New Formalization of Power Series in Coq. The 5th Coq Workshop, Jul 2013, Rennes, France. 2013, <http://coq.inria.fr/coq-workshop/2013>. <hal-00880212>

Partager

Métriques

Consultations de
la notice

164

Téléchargements du document

86