↓ Skip to main content

Intelligent Computer Mathematics

Overview of attention for book
Cover of 'Intelligent Computer Mathematics'

Table of Contents

  1. Altmetric Badge
    Book Overview
  2. Altmetric Badge
    Chapter 1 Enumeration of AG-Groupoids
  3. Altmetric Badge
    Chapter 2 Retargeting OpenAxiom to Poly/ML: Towards an Integrated Proof Assistants and Computer Algebra System Framework
  4. Altmetric Badge
    Chapter 3 Incidence Simplicial Matrices Formalized in Coq/SSReflect
  5. Altmetric Badge
    Chapter 4 Proof Assistant Decision Procedures for Formalizing Origami
  6. Altmetric Badge
    Chapter 5 Using Theorema in the Formalization of Theoretical Economics
  7. Altmetric Badge
    Chapter 6 View of Computer Algebra Data from Coq
  8. Altmetric Badge
    Chapter 7 Computer certified efficient exact reals in Coq
  9. Altmetric Badge
    Chapter 8 A Foundational View on Integration Problems
  10. Altmetric Badge
    Chapter 9 Efficient Formal Verification of Bounds of Linear Programs
  11. Altmetric Badge
    Chapter 10 Large Formal Wikis: Issues and Solutions
  12. Altmetric Badge
    Chapter 11 Licensing the Mizar Mathematical Library
  13. Altmetric Badge
    Chapter 12 Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics
  14. Altmetric Badge
    Chapter 13 Parsing and Disambiguation of Symbolic Mathematics in the Naproche System
  15. Altmetric Badge
    Chapter 14 Interleaving Strategies
  16. Altmetric Badge
    Chapter 15 Combining Source, Content, Presentation, Narration, and Relational Representation
  17. Altmetric Badge
    Chapter 16 Indexing and Searching Mathematics in Digital Libraries
  18. Altmetric Badge
    Chapter 17 Isabelle as Document-Oriented Proof Assistant
  19. Altmetric Badge
    Chapter 18 Towards Formal Proof Script Refactoring
  20. Altmetric Badge
    Chapter 19 mizar-items : Exploring Fine-Grained Dependencies in the Mizar Mathematical Library
  21. Altmetric Badge
    Chapter 20 Formalization of Formal Topology by Means of the Interactive Theorem Prover Matita
  22. Altmetric Badge
    Chapter 21 Project EuDML – A First Year Demonstration
  23. Altmetric Badge
    Chapter 22 A Symbolic Companion for Interactive Geometric Systems
  24. Altmetric Badge
    Chapter 23 MathScheme: Project Description
  25. Altmetric Badge
    Chapter 24 Project Abstract: Logic Atlas and Integrator (LATIN)
  26. Altmetric Badge
    Chapter 25 The LaTeXML Daemon: Editable Math on the Collaborative Web
  27. Altmetric Badge
    Chapter 26 A System for Computing and Reasoning in Algebraic Topology
  28. Altmetric Badge
    Chapter 27 Learning2Reason
  29. Altmetric Badge
    Chapter 28 A Formal ization of the C99 Standard in HOL, Isabelle and Coq
  30. Altmetric Badge
    Chapter 29 Krextor - An Extensible Framework for Contributing Content Math to the Web of Data
  31. Altmetric Badge
    Chapter 30 System Description: EgoMath2 As a Tool for Mathematical Searching on Wikipedia.org
Attention for Chapter 7: Computer certified efficient exact reals in Coq
Altmetric Badge

About this Attention Score

  • Above-average Attention Score compared to outputs of the same age (58th percentile)
  • Good Attention Score compared to outputs of the same age and source (76th percentile)

Mentioned by

2 tweeters
1 Redditor


6 Dimensions

Readers on

8 Mendeley
You are seeing a free-to-access but limited selection of the activity Altmetric has collected about this research output. Click here to find out more.
Chapter title
Computer certified efficient exact reals in Coq
Chapter number 7
Book title
Intelligent Computer Mathematics
Published in
arXiv, May 2011
DOI 10.1007/978-3-642-22673-1_7
Book ISBNs
978-3-64-222672-4, 978-3-64-222673-1

Robbert Krebbers, Bas Spitters


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.

Twitter Demographics

The data shown below were collected from the profiles of 2 tweeters who shared this research output. Click here to find out more about how the information was compiled.

Mendeley readers

The data shown below were compiled from readership statistics for 8 Mendeley readers of this research output. Click here to see the associated Mendeley record.

Geographical breakdown

Country Count As %
Japan 1 13%
Austria 1 13%
Unknown 6 75%

Demographic breakdown

Readers by professional status Count As %
Student > Ph. D. Student 4 50%
Student > Master 2 25%
Researcher 2 25%
Readers by discipline Count As %
Computer Science 5 63%
Mathematics 3 38%

Attention Score in Context

This research output has an Altmetric Attention Score of 2. This is our high-level measure of the quality and quantity of online attention that it has received. This Attention Score, as well as the ranking and number of research outputs shown below, was calculated when the research output was last mentioned on 21 January 2013.
All research outputs
of 6,643,327 outputs
Outputs from arXiv
of 384,502 outputs
Outputs of similar age
of 67,425 outputs
Outputs of similar age from arXiv
of 2,592 outputs
Altmetric has tracked 6,643,327 research outputs across all sources so far. This one has received more attention than most of these and is in the 58th percentile.
So far Altmetric has tracked 384,502 research outputs from this source. They receive a mean Attention Score of 2.5. This one has done well, scoring higher than 79% of its peers.
Older research outputs will score higher simply because they've had more time to accumulate mentions. To account for age we can compare this Altmetric Attention Score to the 67,425 tracked outputs that were published within six weeks on either side of this one in any source. This one has gotten more attention than average, scoring higher than 58% of its contemporaries.
We're also able to compare this research output to 2,592 others from the same source and published within six weeks on either side of this one. This one has done well, scoring higher than 76% of its contemporaries.