C. Development and T. , The Coq Reference Manual, Version 8

M. Dauchet, Termination of rewriting is undecidable in the one-rule case, Proceedings of the 13th International Symposium on Mathematical Foundations of Computer Science, 1988.

N. Dershowitz and J. Jouannaud, Rewrite Systems, Handbook of Theoretical Computer Science, J. van Leeuwen, issue.6, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

F. Blanqui and A. Koprowski, CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, Mathematical Structures in Computer Science, vol.37, issue.04, pp.827-859, 2011.
DOI : 10.1016/S0890-5401(03)00011-7
URL : https://hal.archives-ouvertes.fr/inria-00543157

X. Leroy, D. Doligez, A. Frisch, J. Garrigue, D. Rémy et al., The Objective Caml system release 3.12, Documentation and user's manual, 2010.

S. Peyton-jones and E. , Haskell 98 Language and Libraries, The revised report, 2003.

M. Sperber, R. K. Dybvig, M. Flatt, A. Van-straaten, R. Findler et al., Revised6 Report on the Algorithmic Language Scheme, Journal of Functional Programming, vol.4, issue.S1, pp.1-301, 2004.
DOI : 10.1023/A:1010051815785

C. Sternagel, R. Thiemann, S. Winkler, and H. Zankl, CeTA 2.4, p.2012

T. Nipkow, L. Paulson, M. Wenzel, /. Isabelle, and . Hol, A Proof Assistant for Higher-Order Logic, ser. Lecture Notes in Computer Science, 2002.

F. Haftmann, Code generation from specifications in higher order logic, 2009.

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

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

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, Proceedings of the 1st International Conference on Typed Lambda Calculi and Applications, 1993.
DOI : 10.1007/BFb0037116

D. Lankford, On proving term rewriting systems are noetherian, 1979.

E. Contejean, C. Marché, A. P. Tomás, and X. Urbain, Mechanically Proving Termination Using Polynomial Interpretations, Journal of Automated Reasoning, vol.12, issue.1, pp.325-363, 2005.
DOI : 10.1007/s10817-005-9022-x
URL : https://hal.archives-ouvertes.fr/inria-00001167

T. Arts and J. Giesl, Termination of term rewriting using dependency pairs, Theoretical Computer Science, vol.236, issue.1-2, pp.133-178, 2000.
DOI : 10.1016/S0304-3975(99)00207-8

R. Thiemann and J. Giesl, The size-change principle and dependency pairs for termination of term rewriting, Applicable Algebra in Engineering, Communication and Computing, vol.25, issue.4, pp.229-270, 2005.
DOI : 10.1007/s00200-005-0179-7

N. Hirokawa and A. Middeldorp, Tyrolean termination tool: Techniques and features, Information and Computation, vol.205, issue.4, pp.474-511, 2007.
DOI : 10.1016/j.ic.2006.08.010

J. Giesl, R. Thiemann, and P. Schneider-kamp, The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs, Proceedings of the 11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2004.
DOI : 10.1007/978-3-540-32275-7_21

J. Siméon and P. Wadler, The essence of XML, Proceedings of the 30th ACM Symposium on Principles of Programming Languages, 2003.

G. Barthe, P. Courtieu, G. Dufay, and S. De-sousa, Tool-Assisted Specification and Verification of the JavaCard Platform, Proceedings of the 9th International Conference on Algebraic Methodology and Software Technology, Lecture Notes in Computer Science 2422, 2002.
DOI : 10.1007/3-540-45719-4_4

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Proceedings of the 8th Asian Symposium on Computer Mathematics, 2007.
DOI : 10.1007/978-3-540-87827-8_28

T. C. Hales, J. Harrison, S. Mclaughlin, T. Nipkow, S. Obua et al., A Revision of the Proof of the Kepler Conjecture, Discrete & Computational Geometry, vol.70, issue.4, pp.1-34, 2005.
DOI : 10.1007/s00454-009-9148-4

J. Girard, Y. Lafont, and P. Taylor, Proofs and Types, 1988.

P. Martin-löf, Intuitionistic type theory, 1984.

C. Cornes, Conception d'un langage de haut niveau de représentation de preuves, 1997.

D. Delahaye, A Tactic Language for the System Coq, Proceedings of the 7th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 1955.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

P. Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, pp.461-493, 1992.
DOI : 10.1145/91556.91592

S. Glondu, Vers une certification de l'extraction de Coq, Cannasse and J. Garrigue, 2012.

F. Blanqui, T. Hardin, and P. Weis, On the Implementation of Construction Functions for Non-free Concrete Data Types, Proceedings of the 16th European Symposium on Programming, 2007.
DOI : 10.1007/978-3-540-71316-6_8
URL : https://hal.archives-ouvertes.fr/inria-00095110

A. Frisch, G. Castagna, and V. Benzaken, Semantic subtyping, Journal of the ACM, vol.55, issue.4, pp.1-64, 2008.
DOI : 10.1145/1391289.1391293
URL : https://hal.archives-ouvertes.fr/hal-00152690

E. Ohlebusch, A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems, Bulletin of EATCS, vol.50, pp.223-228, 1993.