S. Abian and A. B. Brown, A theorem on partially ordered sets, with applications to fixed point theorems, Journal canadien de math??matiques, vol.13, issue.0, pp.78-82, 1961.
DOI : 10.4153/CJM-1961-007-5

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

R. C. Backhouse, Fixed point calculus, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, 2002.
DOI : 10.1007/3-540-60164-3_25
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.8300

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, Theorem-proving support in programming language semantics, 2007.
DOI : 10.1017/CBO9780511770524.016
URL : https://hal.archives-ouvertes.fr/inria-00160309

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

Y. Bertot and V. Komendantsky, Proofs on domain theory and partial recursion, 2008.

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.

A. Bove and V. Capretta, Computation by Prophecy, Typed Lambda Calculi and Applications, 8th International Conference Proceedings, pp.70-83, 2007.
DOI : 10.1007/978-3-540-73228-0_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.2242

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

D. Clément, J. Despeyroux, T. Despeyroux, and G. Kahn, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming , LFP '86, 1986.
DOI : 10.1145/319838.319847

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

S. Glondu, Garantie formelle de correction pour l'extraction Coq, 2007.

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

A. Megacz, A coinductive monad for prop-bounded recursion, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.11-20, 2007.
DOI : 10.1145/1292597.1292601

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

H. R. 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, pp.605-619, 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, A constructive denotational semantics for Kahn networks in Coq, 2007.
DOI : 10.1017/CBO9780511770524.018
URL : https://hal.archives-ouvertes.fr/inria-00431806

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

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

F. Regensburger, 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