P. Aczel, An Introduction to Inductive Definitions, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, 1977.
DOI : 10.1016/S0049-237X(08)71120-0

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.

Y. Bertot and P. Castéran, Interactive theorem proving and program development , Coq'art: the calculus of inductive constructions. Texts in Theoretical Computer Science: an EATCS series, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Bove, General recursion in type theory The Netherlands, number 2646 in Lecture Notes in Computer Science, Types for Proofs and Programs, International Workshop TYPES 2002, pp.39-58, 2003.

J. Camilleri and T. Melham, Reasoning with inductively defined relations in the HOL theorem prover, 1992.

L. Chicli, L. Pottier, and C. Simpson, Mathematical Quotients and Quotient Types in Coq, Types for Proofs and Programs, number 2646 in LNCS, pp.95-107, 2003.
DOI : 10.1007/3-540-39185-1_6

C. Dubois and V. Viguié-donzeau-gouge, A step towards the mechanization of partial functions: domains as inductive predicates, 1998.

J. Harrison, Inductive definitions: Automation and application, Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Sciences, 1995.
DOI : 10.1007/3-540-60275-5_66

G. Huet, Induction principles formalized in the calculus of constructions, TAPSOFT'87, pp.276-286, 1987.
DOI : 10.1007/3-540-17660-8_62

G. Kahn, Elements of constructive geometry group theory and domain theory, 1995.

P. Letouzey, A New Extraction for Coq, Lecture Notes in Computer Science, vol.2646, 2002.
DOI : 10.1007/3-540-39185-1_12
URL : https://hal.archives-ouvertes.fr/hal-00150914

O. Müller, T. Nipkow, O. David-von-oheimb, . Slotosch, . Holcf et al., HOLCF = HOL + LCF, Journal of Functional Programming, vol.9, issue.2, pp.191-223, 1999.
DOI : 10.1017/S095679689900341X

H. Nielson and F. Nielson, Semantics with Applications: A Formal Introduction, 1992.

T. Nipkow, Winskel is (almost) Right: Towards a Mechanized Semantics Textbook, Formal Aspects of Computing, vol.10, issue.2, pp.171-186, 1998.
DOI : 10.1007/s001650050009

B. Nordström, Terminating general recursion, BIT, vol.24, issue.3, 1988.
DOI : 10.1007/BF01941137

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Proceedings of the conference Typed Lambda Calculi and Applications, number 664 in Lecture Notes in Computer Science, pp.92-141, 1993.
DOI : 10.1007/BFb0037116

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

C. Lawrence and . Paulson, Logic and computation, Interactive proof with Cambridge LCF, 1987.

F. Regensburger and . Holcf, HOLCF: Higher order logic of computable functions, Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th International Workshop, volume 971 of Lecture Notes in Computer Sciences, 1995.
DOI : 10.1007/3-540-60275-5_72

G. Winskel, The Formal Semantics of Programming Languages, an introduction . Foundations of Computing, 1993.