Floating-point arithmetic in the Coq system

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.
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/hal-01780385
Contributor : Guillaume Melquiond <>
Submitted on : Friday, April 27, 2018 - 2:42:10 PM
Last modification on : Saturday, April 28, 2018 - 1:19:54 AM
Long-term archiving on: Thursday, September 20, 2018 - 5:55:54 AM

File

08-rnc8-article.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01780385, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

97

Files downloads

131