works on
computable analysis 1coq formalization 1exact real computation 1fractal generation 1hyperspaces 1polish spaces 1

From the 1 of 1 linked paper with an AI index.

collaborators

1 paper

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…