4 citations · 10 across the 10 of their papers we have counts for
4 papers · 1 filter
Formalizing Hyperspaces and Operations on Subsets of Polish Spaces over Abstract Exact Real Numbers
Michal Konečný, Sewon Park, Holger Thies
Building on our prior work on axiomatization of exact real computation by formalizing nondeterministic first-order partial computations over real and complex numbers in a construct…
An Imperative Language for Verified Exact Real-Number Computation
Andrej Bauer, Sewon Park, Alex Simpson
We introduce Clerical, a programming language for exact real-number computation that combines first-order imperative-style programming with a limit operator for computation of real…
Extracting efficient exact real number computation from proofs in constructive type theory
Michal Konečný, Sewon Park, Holger Thies
Exact real computation is an alternative to floating-point arithmetic where operations on real numbers are performed exactly, without the introduction of rounding errors. When prov…
Computable Operations on Compact Subsets of Metric Spaces with Applications to Fréchet Distance and Shape Optimization
Chansu Park, Ji-Won Park, Sewon Park +2
We extend the Theory of Computation on real numbers, continuous real functions, and bounded closed Euclidean subsets, to compact metric spaces : thereby generically includin…