License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2019.7
URN: urn:nbn:de:0030-drops-110629
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2019/11062/
Go to the corresponding LIPIcs Volume Portal

Bertholon, Guillaume ; Martin-Dorel, Érik ; Roux, Pierre

Primitive Floats in Coq

pdf-format:
LIPIcs-ITP-2019-7.pdf (0.6 MB)

Abstract

Some mathematical proofs involve intensive computations, for instance: the four-color theorem, Hales' theorem on sphere packing (formerly known as the Kepler conjecture) or interval arithmetic. For numerical computations, floating-point arithmetic enjoys widespread usage thanks to its efficiency, despite the introduction of rounding errors.
Formal guarantees can be obtained on floating-point algorithms based on the IEEE 754 standard, which precisely specifies floating-point arithmetic and its rounding modes, and a proof assistant such as Coq, that enjoys efficient computation capabilities. Coq offers machine integers, however floating-point arithmetic still needed to be emulated using these integers.
A modified version of Coq is presented that enables using the machine floating-point operators. The main obstacles to such an implementation and its soundness are discussed. Benchmarks show potential performance gains of two orders of magnitude.

BibTeX - Entry

@InProceedings{bertholon_et_al:LIPIcs:2019:11062,
  author =	{Guillaume Bertholon and {\'E}rik Martin-Dorel and Pierre Roux},
  title =	{{Primitive Floats in Coq}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{7:1--7:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11062},
  URN =		{urn:nbn:de:0030-drops-110629},
  doi =		{10.4230/LIPIcs.ITP.2019.7},
  annote =	{Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition}
}

Keywords: Coq formal proofs, floating-point arithmetic, reflexive tactics, Cholesky decomposition
Collection: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue Date: 2019
Date of publication: 05.09.2019
Supplementary Material: https://github.com/coq/coq/pull/9867

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI