@inproceedings{ac9f5480462a41ef96a123172881c457,
title = "Computer certified efficient exact reals in Coq",
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.",
author = "Robbert Krebbers and Bas Spitters",
year = "2011",
month = aug,
day = "11",
doi = "10.1007/978-3-642-22673-1_7",
language = "English",
isbn = "9783642226724",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "90--106",
booktitle = "Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011 and 10th International Conference, MKM 2011, Proceedings",
note = "18th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning, Calculemus 2011 and 10th International Conference on Mathematical Knowledge Management, MKM 2011 ; Conference date: 18-07-2011 Through 23-07-2011",
}