Certified Exact Transcendental Real Number Computation in Coq
From MaRDI portal
Publication:3543662
DOI10.1007/978-3-540-71067-7_21zbMath1165.68466arXiv0805.2438OpenAlexW3099251155MaRDI QIDQ3543662
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
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
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
