Enabling Floating-Point Arithmetic in the Coq Proof Assistant - Fiabilité des Systèmes et des Logiciels Access content directly
Journal Articles Journal of Automated Reasoning Year : 2023

Enabling Floating-Point Arithmetic in the Coq Proof Assistant

Abstract

Floating-point arithmetic is a well-known and extremely efficient way of performing approximate computations over the real numbers. Although it requires some careful considerations, floating-point numbers are nowadays routinely used to prove mathematical theorems. Numerical computations have been applied in the context of formal proofs too, as illustrated by the CoqInterval library. But these computations do not benefit from the powerful floating-point units available in modern processors, since they are emulated inside the logic of the formal system. This paper experiments with the use of hardware floating-point numbers for numerically intensive proofs verified by the Coq proof assistant. This gives rise to various questions regarding the formalization, the implementation, the usability, and the level of trust. This approach has been applied to the CoqInterval and ValidSDP libraries, which demonstrates a speedup of at least one order of magnitude.
Fichier principal
Vignette du fichier
article.pdf (455.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-04114233 , version 1 (01-06-2023)
hal-04114233 , version 2 (31-08-2023)

Licence

Attribution

Identifiers

Cite

Érik Martin-Dorel, Guillaume Melquiond, Pierre Roux. Enabling Floating-Point Arithmetic in the Coq Proof Assistant. Journal of Automated Reasoning, 2023, 67 (33), ⟨10.1007/s10817-023-09679-x⟩. ⟨hal-04114233v2⟩
158 View
113 Download

Altmetric

Share

Gmail Facebook X LinkedIn More