T. Coquand, An analysis of girard's paradox, Symposium on Logic in Computer Science, 1986.

T. Coquand, Metamathematical Investigations of a Calculus of Constructions, Logic and Computer Science, pp.91-122, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00075471

E. Giménez, Codifying guarded definitions with recursive schemes, Workshop on Types for Proofs and Programs, number 996 in LNCS, pp.39-59, 1994.
DOI : 10.1007/3-540-60579-7_3

E. Giménez, An application of co-inductive types in Coq: Verification of the alternating bit protocol, Workshop on Types for Proofs and Programs, number 1158 in LNCS, pp.135-152, 1995.
DOI : 10.1007/3-540-61780-9_67

E. Giménez, A Calculus of Infinite Constructions and its application to the verification of communicating systems, 1996.

G. Huet, G. Kahn, and C. Paulin-mohring, The Coq proof assistant -a tutorial, version 6.1. rapport technique 204, 1997.
URL : https://hal.archives-ouvertes.fr/inria-00069967

I. Unité-de-recherche, . Lorraine, V. Technopôle-de-nancy-brabois, I. Unité-de-recherche, and . Rennes, Campus scientifique, 615 rue du Jardin Botanique Irisa, Campus universitaire de Beaulieu, 35042 RENNES Cedex Unité de recherche INRIA Rhône-Alpes, 2004.