Axiomatic reals and certified efficient exact real computation

DOI10.1007/978-3-030-88853-4_16MaRDI QIDQ2148797zbMATH OpenOpenAlexFDO

Authors Michal Konečný, Holger Thies, Se Won Park

Publication date 24 June 2022

Full work available at URL https://doi.org/10.1007/978-3-030-88853-4_16

zbMATH Keywords

program extractionformal proofsexact real number computationconstructive real numbers

Mathematics Subject Classification ID

Logic in computer science (03B70)

Recommendations

• A certified, corecursive implementation of exact real numbers
• Computer Certified Efficient Exact Reals in Coq
• From coinductive proofs to exact real arithmetic: theory and applications
• From Coinductive Proofs to Exact Real Arithmetic
• Logic for exact real arithmetic

Cites work

• scientific article; zbMATH DE number 1302063 (Why is no real title available?)
• scientific article; zbMATH DE number 2079044 (Why is no real title available?)
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 1497733 (Why is no real title available?)
• scientific article; zbMATH DE number 1746043 (Why is no real title available?)
• A Real Number Structure that is Effectively Categorical
• A fundamental effect in computations on real numbers
• Combining Coq and Gappa for Certifying Floating-Point Programs
• Computable analysis and notions of continuity in \textsc{Coq}
• Computational complexity of real powering and improved solving linear differential equations
• Constructive analysis with witnesses
• Effectivity in Spaces with Admissible Multirepresentations
• Feasible real random access machines
• Formalization of real analysis: a survey of proof assistants and libraries
• Locally cartesian closed categories and type theory
• Mathematical Knowledge Management
• Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
• Proving Bounds on Real-Valued Functions with Computations
• Realizability. An introduction to its categorical side
• Theory of representations

Cited in

(9)

• Efficient Exact Arithmetic over Constructive Reals
• Verified Real Asymptotics in Isabelle/HOL
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis
• Certified Exact Transcendental Real Number Computation in Coq
• Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base
• Computer Certified Efficient Exact Reals in Coq
• A Coq formalization of Taylor models and power series for solving ordinary differential equations
• Extracting efficient exact real number computation from proofs in constructive type theory
• Verified exact real computation with nondeterministic functions and limits

Describes a project that uses

Uses Software

• iRRAM
• Flocq
• C-CoRN
• Ariadne
• Gappa
• Haskell
• Coq

This page was built for publication: Axiomatic reals and certified efficient exact real computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2148797)