computable analysis 1coq formalization 1exact real computation 1fractal generation 1hyperspaces 1polish spaces 1
From the 1 of 2 linked papers with an AI index.
2 papers
math.NA2026
Algorithmic Cost in "Exact Real Computation"
Jihoon Hyun, Holger Thies, Martin Ziegler
Turing completeness of a programming language or system characterizes its expressive power; and the strong Church-Turing hypo-/thesis refines such from qualitative to polynomial-ti…
cs.LO2026
Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers
Michal KoneÄný, Sewon Park, Holger Thies
The paper develops a Coq formalization for exact real computation on hyperspaces of subsets of Polish spaces, defining open, closed, compact, and overt sets and extracting certifie…