A. Abel, Type-Based Termination. A Polymorphic Lambda-Calculus with Sized Higher-Order Types, 2006.

P. Aczel, An Introduction to Inductive Definitions, Handbook of Mathematical Logic, pp.739-782, 1977.
DOI : 10.1016/S0049-237X(08)71120-0

P. Aczel, Algebras and Coalgebras, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, pp.79-88, 2000.
DOI : 10.1007/3-540-47797-7_3

A. Balaa and Y. Bertot, Fixpoint equations for well-founded recursion in type theory, Theorem Proving in Higher-Order Logics: 13th International Conference, pp.1-16, 2000.

A. Balaa and Y. Bertot, Fonctions récursives générales par itération en théorie des types, Journées Francophones pour les Langages Applicatifs, 2002.

H. Barendregt, Lambda calculi with types, Handbook of Logic in Computer Science, volume II, pp.117-309, 1992.
DOI : 10.1017/cbo9781139032636

H. Barendregt and H. Geuvers, Proof-checking using dependent type systems, Handbook of Automated Reasoning, volume II, chapter 18, pp.1149-1240, 2001.
DOI : 10.1016/b978-044450813-3/50020-5
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.17.7813

G. Barthe, The relevance of proof-irrelevance, Authomata, Languages and Programming (ICALP'98), pp.755-768, 1998.
DOI : 10.1007/BFb0055099

G. Barthe, M. J. Frade, E. Giménez, L. Pinto, and T. Uustalu, Type-based termination of recursive definitions, Mathematical Structures in Computer Science, vol.14, issue.1, pp.97-141, 2004.
DOI : 10.1017/S0960129503004122

Y. Bertot, Filters and co-inductive streams, an application to eratosthenes' sieve, TLCA, pp.102-115, 2005.
DOI : 10.1007/11417170_9
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.99.5339

Y. Bertot, Affine functions and series with co-inductive real numbers, Mathematical Structures in Computer Science, vol.17, issue.01, pp.37-63, 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 Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot and E. Komendantskaya, Experiments towards general co-recursion: Coq code, 2008.
DOI : 10.1007/978-3-662-07964-5_15

A. Bove, Simple general recursion in type theory, Nordic Journal of Computing, vol.8, issue.1, pp.22-42, 2001.

A. Bove, General Recursion in Type Theory, 2002.
DOI : 10.1007/3-540-39185-1_3

A. Bove, General Recursion in Type Theory, TYPES, pp.39-58, 2002.
DOI : 10.1007/3-540-39185-1_3

A. Bove and V. Capretta, Nested General Recursion and Partiality in Type Theory, TPHOLs, pp.121-135, 2001.
DOI : 10.1007/3-540-44755-5_10
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.1831

A. Bove and V. Capretta, Modelling general recursion in type theory, Mathematical Structures in Computer Science, vol.15, issue.4, pp.671-708, 2005.
DOI : 10.1017/S0960129505004822

W. Buchholz, A term calculus for (co-)recursive definitions on streamlike data structures, Annals of Pure and Applied Logic, vol.136, issue.1-2, pp.75-90, 2005.
DOI : 10.1016/j.apal.2005.05.006

V. Capretta, General recursion via coinductive types, Logical Methods in Computer Science, vol.1, issue.2, 2005.
DOI : 10.2168/LMCS-1(2:1)2005
URL : http://arxiv.org/abs/cs/0505037

T. Coquand, Pattern-matching in type theory, Informal Proceedings of the 1992 workshop on Types for Proofs and Programs, pp.71-84, 1992.

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

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

E. Dijkstra, On the productivity of recursive definitions, p.749, 1980.

A. Edalat and J. Potts, A New Representation for Exact Real Numbers, MFPS XIII, 1997.
DOI : 10.1016/S1571-0661(05)80166-5

J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, and J. W. Klop, Productivity of stream definitions, FCT, pp.274-287, 2007.
DOI : 10.1016/j.tcs.2009.10.014
URL : http://doi.org/10.1016/j.tcs.2009.10.014

H. Geuvers, Logics and Type Systems, 1993.

P. D. Gianantonio, A Functional Approach to Computability on Real Numbers, 1993.

P. D. Gianantonio and M. Miculan, A Unifying Approach to Recursive and Co-recursive Definitions, TYPES, pp.148-161, 2002.
DOI : 10.1007/3-540-39185-1_9

P. D. Gianantonio and M. Miculan, Unifying Recursive and Co-recursive Definitions in Sheaf Categories, FoSSaCS, pp.136-150, 2004.
DOI : 10.1007/978-3-540-24727-2_11

E. Gimenez, Un Calcul de Constructions Infinies et son Application a la Verification des Systemes Communcants, 1996.

W. Howard, The formulae-as-types notion of construction, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp.479-490, 1980.

G. Huet, Induction principles formalised in calculus of constructions, To H.B. Curry: Essays on Combinatory Logic, Lmabda Calculus, and formalism, pp.479-490, 1988.

B. Jacobs, Exercises in Coalgebraic Specification, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, number 2297 in LNCS, pp.237-280, 2002.
DOI : 10.1007/3-540-47797-7_7

B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, pp.222-259, 1997.

J. Matthews, Recursive Function Definition over Coinductive Types, TPHOLs, pp.73-90, 1999.
DOI : 10.1007/3-540-48256-3_6

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, Coinductive Field of Exact Real Numbers and General Corecursion, Proc. of CMCS'06, pp.121-139, 2006.
DOI : 10.1016/j.entcs.2006.06.008

B. Nordstö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, TLCA, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

L. Paulson, Mechanizing coinduction and corecursion in higher-order logic, Logic and Computation, pp.175-204, 1997.
DOI : 10.1093/logcom/7.2.175

A. Pnueli, The temporal semantics of concurrent programs, Theoretical Computer Science, issue.31, pp.45-60, 1981.

B. Sijtsma, On the productivity of recursive list definitions, ACM Transactions on Programming Languages and Systems, vol.11, issue.4, pp.633-649, 1989.
DOI : 10.1145/69558.69563