Limits of real numbers in the binary signed digit representation

Franziskus Wiesnet, Nils Köpp

We extract verified algorithms for exact real number computation from constructive proofs. To this end we use a coinductive representation of reals as streams of binary signed digi…