G. Barthe, M. Ruys, and H. Barendregt, A two-level approach towards lean proofchecking, TYPES '95 : Selected papers from the International Workshop on Types for Proofs and Programs, pp.16-35, 1996.
DOI : 10.1007/3-540-61780-9_59
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.23.3434

A. Bauer, M. H. Escardó, and A. Simpson, Comparing Functional Paradigms for Exact Real-Number Computation, Automata, languages and programming, pp.489-500, 2002.
DOI : 10.1007/3-540-45465-9_42
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.100.3797

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes??? Sieve, Typed Lambda Calculi and Applications, pp.102-115, 2005.
DOI : 10.1007/11417170_9
URL : https://hal.archives-ouvertes.fr/inria-00070658

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development, Coq'Art :the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

H. Boehm, R. Cartwright, M. Riggle, and M. J. Donnell, Exact real arithmetic: a case study in higher order programming, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, pp.162-173, 1986.
DOI : 10.1145/319838.319860

S. Boldo, Preuves formelles en arithmétiquesarithmétiques`arithmétiquesàvirgule flottante, 2004.

S. Boldo, M. Daumas, C. Moreau-finot, and L. Théry, Computer validated proofs of a toolset for adaptable arithmetic, Journal of the ACM, 2002.
URL : https://hal.archives-ouvertes.fr/hal-00018530

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS'97, 1997.
DOI : 10.1007/BFb0014565
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7587

A. Ciaffaglione and P. D. Gianantonio, A coinductive approach to real numbers, Types 1999 Workshop, pp.114-130, 1956.
DOI : 10.1007/3-540-44557-9_7

M. Daumas, L. Rideau, and L. Théry, A Generic Library for Floating-Point Numbers and Its Application to Exact Computing, Theorem Proving in Higher Order Logics : 14th International Conference, pp.169-184, 2001.
DOI : 10.1007/3-540-44755-5_13
URL : https://hal.archives-ouvertes.fr/hal-00157285

D. Delahaye and M. Mayero, Field : une procédure de décision pour les nombres réels en coq, Proceedings of JFLA'2001. INRIA, 2001.

P. Di, G. , and M. Miculan, A unifying approach to recursive and co-recursive definitions, Types for Proofs and Programs, pp.148-161, 2003.

P. Di, G. , and M. Miculan, Unifying recursive and co-recursive definitions in sheaf categories, Foundations of Software Science and Computation Structures, 2004.

G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy et al., The Coq Proof Assistant User's Guide. INRIA, 1993.

A. Edalat and P. Potts, A New Representation for Exact Real Numbers, Electronic Notes in Theoretical Computer Science, 1998.
DOI : 10.1016/S1571-0661(05)80166-5

E. Giménez, Codifying guarded definitions with recursive schemes, Types for proofs and Programs, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

R. W. Gosper, HAKMEM, Item 101 B, 1972.

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, International Conference on Functional Programming 2002, pp.235-246, 2002.

P. Pélissier, G. Hanrot, V. Lefèvre, and P. Zimmermann, The mpfr library

J. Harrison, Formal Verification of IA-64 Division Algorithms, Theorem Proving in Higher Order Logics : 13th International Conference, pp.234-251, 2000.
DOI : 10.1007/3-540-44659-1_15

B. Lambov, RealLib: An efficient implementation of exact real arithmetic, Mathematical Structures in Computer Science, vol.17, issue.01, pp.169-175
DOI : 10.1017/S0960129506005822

V. Ménissier-morain, Arithmétique exacte, conception, algorithmique et performances d'une implémentation informatique en précision arbitraire, Thèse, 1994.

V. Ménissier-morain, Conception et algorithmique d'une représentation d'arithmétique réelle en précision arbitraire, Proceedings of the first conference on real numbers and computers, 1995.

J. Muller, Elementary Functions, Algorithms and implementation, 1997.
URL : https://hal.archives-ouvertes.fr/ensl-00000008

N. Th and . Müller, Implementing exact real numbers efficiently, p.378

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL ? A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

M. Niqui, Formalising Exact Arithmetic : Representations, Algorithms and Proofs, 2004.
DOI : 10.1007/11494645_46
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.6690

C. Lawrence and . Paulson, Mechanizing coinduction and corecursion in higher-order logic, Journal of Logic and Computation, vol.7, pp.175-204, 1997.

M. David and . Russinoff, A Mechanically Checked Proof of IEEE Compliance of the AMD K5 Floating- Point Square Root Microcode. Formal Methods in System Design, pp.75-125, 1999.

E. Jean and . Vuillemin, Exact real computer arithmetic with continued fractions, IEEE Transactions on Computers, vol.39, issue.8, pp.1087-1105, 1990.