Y. Bertot, Calcul de formules affines et de sériesentì eres en arithmétique exacte avec types co-inductifs, Thérèse Hardin et Journées francophones des langages applicatifs. INRIA, 2006.

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

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

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

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

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

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

A. Spiwack, Ajouter des entiers machinè a coq, 2006.

B. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, FLOPS, pp.97-113, 2006.
DOI : 10.1007/11737414_8

V. Menissier-morain and P. Weis, An exact arithmetic package for ml