Certified Exact Transcendental Real Number Computation in Coq

DOI10.1007/978-3-540-71067-7_21zbMath1165.68466arXiv0805.2438OpenAlexW3099251155MaRDI QIDQ3543662

Russell O'Connor

Publication date: 4 December 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/0805.2438

Mathematics Subject Classification ID

Related Items

Optimizing a Certified Proof Checker for a Large-Scale Computer-Generated Proof ⋮ Formal Verification of Exact Computations Using Newton’s Method ⋮ Wave equation numerical resolution: a comprehensive mechanized proof of a C program ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Verified correctness, accuracy, and convergence of a stationary iterative linear solver: Jacobi method ⋮ Formally proving size optimality of sorting networks ⋮ Formalization of real analysis: a survey of proof assistants and libraries ⋮ A computer-verified monadic functional implementation of the integral ⋮ Computer Certified Efficient Exact Reals in Coq ⋮ A certifying square root and division elimination ⋮ Formal proofs for theoretical properties of Newton's method ⋮ A formal study of Bernstein coefficients and polynomials ⋮ Type classes for mathematics in type theory ⋮ Classical mathematics for a constructive world ⋮ Formalizing a discrete model of the continuum in Coq from a discrete geometry perspective

Uses Software

• Coq
• C-CoRN

Cites Work

• Disproof of the Mertens conjecture.
• A monadic, functional implementation of real numbers
• Program Extraction from Large Proof Developments
• Mathematical Knowledge Management
• Real numbers and other completions
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Theorem Proving in Higher Order Logics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item