Computer certified efficient exact reals in Coq
Robbert Krebbers, Bas Spitters

TL;DR
This paper presents an optimized implementation of exact real numbers in Coq, leveraging dyadic rationals and approximate division to significantly improve computational efficiency and usability.
Contribution
It introduces a novel Coq library for exact reals using dyadic rationals and type classes, achieving over 100x speedup and enhancing mathematical interface design.
Findings
Over 100 times speedup in basic operations
Use of dyadic rationals from machine integers
First application of type classes in heavy computation
Abstract
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-implementation by O'Connor in two ways: we use dyadic rationals built from the machine integers and we optimize computation of power series by using approximate division. Moreover, we use type classes for clean mathematical interfaces. This appears to be the first time that type classes are used in heavy computation. We obtain over a 100 times speed up of the basic operations and indications for improving the Coq system.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHermeneutics and Narrative Identity · Aging, Elder Care, and Social Issues · Health, Medicine and Society
