Skip to Main content Skip to Navigation
Journal articles

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 [15 references]  Display  Hide  Download

https://hal.inria.fr/hal-00797913
Contributor : Guillaume Melquiond <>
Submitted on : Thursday, March 7, 2013 - 3:25:03 PM
Last modification on : Wednesday, September 16, 2020 - 5:22:48 PM
Long-term archiving on: : Monday, June 17, 2013 - 11:18:08 AM

File

article.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

514

Files downloads

677