P. Aczel, Non-Well-Founded Sets. CSLI Lecture Notes, 1988.

Y. Bertot, Algebras and Coalgebras. Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, Lecture Notes in Computer Science, vol.2297, 2002.

Y. Bertot, Filters on CoInductive Streams, an Application to Eratosthenes' Sieve. Typed Lamdba-Calculi and Applications'05, Lecture Notes in Computer Science, vol.3461, 2005.
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

P. Castéran and D. Rouillard, Reasoning about parametrized automata, Proceedings, 8-th International Conference on Real-Time System, pp.107-119, 2000.

A. Ciaffaglione and P. D. Gianantonio, A Co-Inductive Approach to Real Numbers. Types for Proofs and Programs, Lecture Notes in Computer Science, vol.1956, 2000.

T. Coquand, Infinite objects in Type Theory. Types for Proofs and Programs, Lecture Notes in Computer Science, vol.806, 1993.

S. Coupet, An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions, Journal of Logic and Computation, vol.13, issue.6, pp.801-813, 2003.
DOI : 10.1093/logcom/13.6.801

S. Coupet-grimal and L. Jakubiec, Hardware Verification Using Co-induction in COQ, TPHOLs'99, 1999.
DOI : 10.1007/3-540-48256-3_7

A. Edalat and R. Heckmann, Computing with Real Numbers Applied semantics, Lecture Notes in Computer Science, vol.2395, 2002.
DOI : 10.1007/3-540-45699-6_5

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.

E. Giménez, Codifying guarded definitions with recursive schemes. Types for Proofs and Programs, Lecture Notes in Computer Science, vol.996, 1994.

E. Giménez, An Application of Co-Inductive Types in Coq: Verification of the Alternating Bit Protocol. Types for Proofs and Programs, Lecture Notes in Computer Science, vol.1158, 1995.

J. Hughes and M. Niqui, Admissible digit sets. To appear in Theoretical Computer Science, special issue on real numbers and computers, 2005.
DOI : 10.1016/j.tcs.2005.09.059
URL : http://doi.org/10.1016/j.tcs.2005.09.059

F. Leclerc and C. Paulin-mohring, Programming with streams in coq. A case study: the sieve of Eratosthenes. Types for Proofs and Progams, Lecture Notes in Computer Science, vol.806, 1993.

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

M. Niqui, Formalising Exact Arithmetic in Type Theory. First conference on computability in Europe, Lecture Notes in Computer Science, vol.3526, 2005.

C. Lawrence and . Paulson, A fixedpoint approach to implementing (co)inductive definitions, Conference on Automated Deduction, 1994.