A. Bauer, M. 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

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, O. Donnell, and M. J. , 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à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, volume 1281, 1997.
DOI : 10.1007/BFb0014565
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7587

A. Ciaffaglione and P. Di-gianantonio, A coinductive approach to real numbers, Types 1999 Workshop, pp.114-130, 1956.

T. Coquand, Infinite objects in type theory, Types for Proofs and Programs, pp.62-78, 1993.
DOI : 10.1007/3-540-58085-9_72

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the Constructive Coq Repository at Nijmegen, Lecture Notes in Computer Science, vol.3119, pp.88-103, 2004.
DOI : 10.1007/3-540-45620-1_12

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-gianantonio, A golden ration notation for the real numbers, 1996.

P. Di-gianantonio and M. Miculan, A Unifying Approach to Recursive and Co-recursive Definitions, Types for Proofs and Programs, pp.148-161, 2003.
DOI : 10.1007/3-540-39185-1_9

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

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

J. Gibbons, Streaming Representation-Changers, Lecture Notes in Computer Science, vol.3125, pp.142-168, 2004.
DOI : 10.1007/978-3-540-27764-4_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.5.818

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.

T. Hales, The flyspeck project fact sheet, 2004.

T. C. Hales, Cannonballs and honeycombs, Notices of the AMS, vol.47, issue.4, pp.440-449, 2000.

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

J. Harrison, HOL Light: A tutorial introduction, Lecture Notes in Computer Science, vol.1166, pp.265-269, 1996.
DOI : 10.1007/BFb0031814
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.24.42

J. Harrison, Theorem Proving with the Real Numbers, 1998.
DOI : 10.1007/978-1-4471-1591-5

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 and . Grubba, RealLib: An efficient implementation of exact real arithmetic, Mathematical Structures in Computer Science, vol.17, issue.01, pp.169-175, 2005.
DOI : 10.1017/S0960129506005822

A. Mahboubi, Programming and certifying the CAD algorithm inside the Coq system, Mathematical Structures in Computer Science, 2006.

A. Mahboubi and L. Pottier, limination des quantificateurs sur les rels en Coq, Journées Francophones des Langages Applicatifs, 2002.

M. Mayero, Formalisation et automatisation de preuves en analyses réelle et numérique, 2001.

S. Mclaughlin and J. Harrison, A Proof-Producing Decision Procedure for Real Arithmetic, CADE-20: 20th International Conference on Automated Deduction, proceedings, pp.295-314, 2005.
DOI : 10.1007/11532231_22

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. T. Müller and . Grubba, Implementing exact real numbers efficiently, p.378, 2005.

M. Niqui, Formalising Exact Arithmetic, Representations, Algorithms, and Proofs, 2004.

B. Nordström, Terminating general recursion, BIT, vol.24, issue.3, pp.605-619, 1988.
DOI : 10.1007/BF01941137

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science. LIP research report, pp.92-141, 1993.
DOI : 10.1007/BFb0037116

D. M. 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.

J. E. Vuillemin, Exact real computer arithmetic with continued fractions, IEEE Transactions on Computers, vol.39, issue.8, pp.1087-1105, 1990.
DOI : 10.1109/12.57047
URL : https://hal.archives-ouvertes.fr/inria-00075792