Floating-point arithmetic in the Coq system

Guillaume Melquiond 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
Abstract : The process of proving some mathematical theorems can be greatly reduced by relying on numerically-intensive computations with a certified arithmetic. This article presents a formalization of floating-point arithmetic that makes it possible to efficiently compute inside the proofs of the Coq system. This certified library is a multi-radix and multi-precision implementation free from underflow and overflow. It provides the basic arithmetic operators and a few elementary functions.
Type de document :
Article dans une revue
Information and Computation, Elsevier, 2012, 216, pp.14-23. 〈10.1016/j.ic.2011.09.005〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00797913
Contributeur : Guillaume Melquiond <>
Soumis le : jeudi 7 mars 2013 - 15:25:03
Dernière modification le : jeudi 5 avril 2018 - 12:30:22
Document(s) archivé(s) le : lundi 17 juin 2013 - 11:18:08

Fichier

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

Identifiants

Collections

Citation

Guillaume Melquiond. Floating-point arithmetic in the Coq system. Information and Computation, Elsevier, 2012, 216, pp.14-23. 〈10.1016/j.ic.2011.09.005〉. 〈hal-00797913〉

Partager

Métriques

Consultations de la notice

293

Téléchargements de fichiers

296