Floating-point arithmetic in the Coq system - Archive ouverte HAL Access content directly
Conference Papers Year : 2008

Floating-point arithmetic in the Coq system

(1)
1

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.
Fichier principal
Vignette du fichier
08-rnc8-article.pdf (171.17 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01780385 , version 1 (27-04-2018)

Identifiers

  • HAL Id : hal-01780385 , version 1

Cite

Guillaume Melquiond. Floating-point arithmetic in the Coq system. 8th Conference on Real Numbers and Computers, Jul 2008, Santiago de Compostela, Spain. pp.93-102. ⟨hal-01780385⟩

Collections

INRIA
70 View
103 Download

Share

Gmail Facebook Twitter LinkedIn More