Computable analysis for verified exact real computation

DOI10.4230/LIPICS.FSTTCS.2020.50MaRDI QIDQ6839852zbMATH OpenFDO

Authors Michal Konečný, Florian Steinberg, Holger Thies

Publication date 23 March 2026

Copyright license Creative Commons Attribution 3.0 Unported

Full work available at URL https://doi.org/10.4230/LIPICS.FSTTCS.2020.50

zbMATH Keywords

computable analysisCoqexact real computationformal proofsproof assistant

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theory of computing (68Qxx)

Cites work

• A certified, corecursive implementation of exact real numbers
• A tutorial on computable analysis
• An introduction to many-valued and fuzzy logic. Semantics, algebras, and derivation systems
• Computational benefit of smoothness: parameterized bit-complexity of numerical operators on analytic functions and Gevrey's hierarchy
• Continuous and monotone machines
• Coquelicot: a user-friendly library of real analysis for Coq
• Feasible real random access machines
• Formalization of real analysis: a survey of proof assistants and libraries
• Formalization techniques for asymptotic reasoning in classical analysis
• scientific article; zbMATH DE number 1460545 (Why is no real title available?)
• scientific article; zbMATH DE number 1746043 (Why is no real title available?)
• Introduction to Interval Analysis
• Mathematical Knowledge Management
• Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
• PCF extended with real numbers
• Proving Bounds on Real-Valued Functions with Computations
• Theory of representations

Cited in

(2)

• Extracting efficient exact real number computation from proofs in constructive type theory
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis

This page was built for publication: Computable analysis for verified exact real computation

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