Skip to Main content Skip to Navigation
Conference papers

A Generic Library for Floating-Point Numbers and Its Application to Exact Computing

Abstract : In this paper we present a general library to reason about floating-point numbers within the Coq system. Most of the results of the library are proved for an arbitrary floating-point format and an arbitrary base. A special emphasis has been put on proving properties for exact computing, i.e. computing without rounding errors.
Document type :
Conference papers
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-00157285
Contributor : Marc Daumas Connect in order to contact the contributor
Submitted on : Monday, June 25, 2007 - 4:48:06 PM
Last modification on : Saturday, September 11, 2021 - 3:17:25 AM
Long-term archiving on: : Thursday, April 8, 2010 - 6:24:26 PM

File

DauRidThe01.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00157285, version 1

Collections

Citation

Marc Daumas, Laurence Rideau, Laurent Thery. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. Theorem Proving in Higher Order Logics, 2001, Edinburgh, United Kingdom. pp.169-184. ⟨hal-00157285⟩

Share

Metrics

Record views

551

Files downloads

672