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.
Cite
CITATION STYLE
Daumas, M., Rideau, L., & Théry, L. (2001). A generic library for floating-point numbers and its application to exact computing. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 169–184). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_13
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
