A. Algirdas and . Avizienis, Signed-digit number representations for fast parallel arithmetic, IRE Transactions on Electronic Computers, vol.10, pp.389-400, 1961.

Y. Bertot, Affine functions and series with co-inductive real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, 2007.
DOI : 10.1017/S0960129506005809
URL : https://hal.archives-ouvertes.fr/inria-00001171

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

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

A. Edalat and R. Heckmann, Computing with Real Numbers, Lecture Notes in Computer Science, vol.2395, pp.193-267, 2000.
DOI : 10.1007/3-540-45699-6_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

B. Grégoire and L. Théry, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, 3rd International Joint Conference on Automated Reasoning (IJCAR), pp.423-437, 2006.
DOI : 10.1007/11814771_36

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

T. Nipkow, G. Bauer, and P. Schultz, Flyspeck I: Tame Graphs, Automated Reasoning, pp.21-35, 2006.
DOI : 10.1007/11814771_4

M. Niqui, Coinductive Correctness of Homographic and Quadratic Algorithms for Exact Real Numbers, Lecture Notes in Computer Science, vol.4502, pp.203-220, 2006.
DOI : 10.1007/978-3-540-74464-1_14

O. Russell and . Connor, A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, vol.17, pp.129-159, 2007.

A. Spiwack, Ajouter des entiers machine coq, 2006.

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