Formalizing hyperspaces for extracting efficient exact real computation

DOI10.4230/LIPICS.MFCS.2023.59MaRDI QIDQ6647692zbMATH OpenFDO

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

Publication date 3 December 2024

Full work available at URL https://doi.org/10.4230/LIPICS.MFCS.2023.59

zbMATH Keywords

computable analysisprogram extractiontype theory

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Cited in

(2)

• A Coq formalization of Taylor models and power series for solving ordinary differential equations
• Computable analysis for extraction of certified programs and its applications

This page was built for publication: Formalizing hyperspaces for extracting efficient exact real computation

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