English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Floating point operations are fast, but require continuous effort on the partof the user in order to ensure that the results are correct. This burden can beshifted away from the user by providing a library of exact analysis in whichthe computer handles the error estimates. Previously, we [Krebbers/Spitters2011] provided a fast implementation of the exact real numbers in the Coq proofassistant. Our implementation improved on an earlier implementation by O'Connorby using type classes to describe an abstract specification of the underlyingdense set from which the real numbers are built. In particular, we used dyadicrationals built from Coq's machine integers to obtain a 100 times speed up ofthe basic operations already. This article is a substantially expanded versionof [Krebbers/Spitters 2011] in which the implementation is extended in thevarious ways. First, we implement and verify the sine and cosine function.Secondly, we create an additional implementation of the dense set based onCoq's fast rational numbers. Thirdly, we extend the hierarchy to capture orderon undecidable structures, while it was limited to decidable structures before.This hierarchy, based on type classes, allows us to share theory on thenaturals, integers, rationals, dyadics, and reals in a convenient way. Finally,we obtain another dramatic speed-up by avoiding evaluation of terminationproofs at runtime.

Type classes for efficient exact real arithmetic in Coq