Computer Certified Efficient Exact Reals in Coq
From MaRDI portal
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.
Recommendations
- Certified Exact Transcendental Real Number Computation in Coq
- Axiomatic reals and certified efficient exact real computation
- A certified, corecursive implementation of exact real numbers
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Coinduction for exact real number computation
- Efficient Exact Arithmetic over Constructive Reals
- From coinductive proofs to exact real arithmetic: theory and applications
- Coinductive Formal Reasoning in Exact Real Arithmetic
- From Coinductive Proofs to Exact Real Arithmetic
Cites work
- A compiled implementation of strong reduction
- A computer-verified monadic functional implementation of the integral
- A constructive theory of continuous domains suitable for implementation
- A large-scale experiment in executing extracted programs
- A monadic, functional implementation of real numbers
- A new look at generalized rewriting in type theory
- Affine functions and series with co-inductive real numbers
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Certified Exact Transcendental Real Number Computation in Coq
- Comprehending monads
- Extending Coq with Imperative Features and Its Application to SAT Verification
- Extraction in Coq: An Overview
- First-Class Type Classes
- Formal Verification of Exact Computations Using Newton’s Method
- From Coinductive Proofs to Exact Real Arithmetic
- Hints in Unification
- How to make ad hoc proof automation less ad hoc
- scientific article; zbMATH DE number 1818513 (Why is no real title available?)
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Packaging Mathematical Structures
- Program extraction from large proof developments
- Real numbers and other completions
- The calculus of constructions
- Type classes for mathematics in type theory
Cited in
(15)- Bellerophon: tactical theorem proving for hybrid systems
- Formally proving size optimality of sorting networks
- Coquelicot: a user-friendly library of real analysis for Coq
- Axiomatic reals and certified efficient exact real computation
- ROSCoq: robots powered by constructive reals
- A certified reduction strategy for homological image processing
- Computing with classical real numbers
- RealLib: An efficient implementation of exact real arithmetic
- Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof
- Certified Exact Transcendental Real Number Computation in Coq
- scientific article; zbMATH DE number 1863383 (Why is no real title available?)
- Type classes for efficient exact real arithmetic in \textsc{Coq}
- Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
- Extracting efficient exact real number computation from proofs in constructive type theory
- Floating-point arithmetic in the Coq system
This page was built for publication: Computer Certified Efficient Exact Reals in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5200110)
