Axiomatic reals and certified efficient exact real computation

DOI10.1007/978-3-030-88853-4_16OpenAlexW3200130299MaRDI QIDQ2148797

Holger Thies, Michal Konečný, 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

formal proofsprogram extractionexact real number computationconstructive real numbers

Mathematics Subject Classification ID

Logic in computer science (03B70)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Realizability. An introduction to its categorical side
• Theory of representations
• A fundamental effect in computations on real numbers
• Feasible real random access machines
• Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
• Computational complexity of real powering and improved solving linear differential equations
• Formalization of real analysis: a survey of proof assistants and libraries
• Locally cartesian closed categories and type theory
• Proving Bounds on Real-Valued Functions with Computations
• Combining Coq and Gappa for Certifying Floating-Point Programs
• A Real Number Structure that is Effectively Categorical
• Effectivity in Spaces with Admissible Multirepresentations
• Mathematical Knowledge Management

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