1: \begin{abstract}

2: We extract verified algorithms for exact real number computation from constructive proofs.

3: To this end we use a coinductive representation of reals as streams of binary signed digits.

4: The main objective of this paper is the formalisation of a constructive proof that real numbers are closed with respect to limits.

5: All the proofs of the main theorem and the first application are  implemented  in  the Minlog  proof  system and the extracted terms are further translated into Haskell.

6: We compare two approaches.

7: The first approach is a direct proof.

8: In the second approach we make use of the representation of reals by a Cauchy-sequence of rationals.

9: Utilizing translations between the two represenation and using the completeness of the Cauchy-reals, the proof is very short.

10: 

11: In both cases  we  use  Minlog's  program  extraction  mechanism to  automatically  extract  a  formally  verified  program  that  transforms  a converging sequence of reals, i.e.~a sequence of streams of binary signed digits together with a modulus of convergence, into the binary signed digit representation of its limit. The correctness of the extracted terms follows directly from the soundness theorem of program extraction.  

12: 

13: As a first application we use the extracted algorithms together with Heron's method

14: to construct an algorithm that computes square roots with respect to the binary signed digit representation.

15: In a second application we use the convergence theorem to show that the signed digit representation of real numbers is closed under multiplication.

16: \end{abstract}

17: