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…