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

G. Barthe and P. Courtieu, Efficient Reasoning about Executable Specifications in Coq, Proceedings of TPHOLs'02, pp.31-46, 2002.
DOI : 10.1007/3-540-45685-6_4

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.

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 on using structural recursion for corecursion: Coq code, 2008.

Y. Bertot and E. Komendantskaya, Inductive and Coinductive Components of Corecursive Functions in Coq, Electronic Notes in Theoretical Computer Science, vol.203, issue.5, pp.25-47, 2008.
DOI : 10.1016/j.entcs.2008.05.018
URL : https://hal.archives-ouvertes.fr/inria-00277075

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

S. Bronson, Posting to Coq club Codata: problem with guardedness condition?, 2008.

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

N. A. Danielsson, Posting to Coq club Codata: problem with guardedness condition?; An ad-hoc approach to productive definitions, p.109, 2008.

E. W. Dijkstra, Hamming's exercise in SASL, 1981.

J. Endrullis, C. Grabmayer, D. Hendriks, A. Isihara, and J. W. Klop, Productivity of stream definitions, Fundamentals of Computation Theory, pp.274-287, 2007.

P. D. Gianantonio and M. Miculan, A unifying approach to recursive and corecursive definitions, TYPES, pp.148-161, 2002.

E. Giménez, Un Calcul de Constructions Infinies et son ApplicationàApplicationà la Vérification des Systèmes Communicants, 1996.

M. J. Gordon and T. F. Melham, Introduction to HOL : a theorem proving environment for higher-order logic, 1993.

J. Hughes, L. Pareto, and A. Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '96, pp.410-423, 1996.
DOI : 10.1145/237721.240882

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

J. Karczmarczuk, Functional differentiation of computer programs. Higher-Order and Symbolic Computation, pp.35-57, 2001.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL -A Proof Assistant for Higher-Order Logic, LNCS, vol.2283, 2002.

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. Nordström, Terminating general recursion, BIT, vol.24, issue.3, pp.605-619, 1988.
DOI : 10.1007/BF01941137

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

F. Regensburger, HOLCF: Higher order logic of computable functions, Theorem Proving in Higher Order Logics, pp.293-307, 1995.
DOI : 10.1007/3-540-60275-5_72

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

K. Slind, Function definition in higher-order logic, Theorem Proving in Higher Order Logics, 1996.
DOI : 10.1007/BFb0105417