F. Barbanera, Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved, Proc. 2nd Int. Workshop on Conditional and Typed Rewriting Systems, 1990.
DOI : 10.1007/3-540-54317-1_96

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of strong normalization and confluence in the algebraic-??-cube, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.406-415, 1994.
DOI : 10.1109/LICS.1994.316049

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, 10th International Conference on Rewriting Techniques and Applications, 1999.
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

F. Blanqui, J. Jouannaud, and M. Okada, Inductive-data-type systems, Theoretical Computer Science, vol.272, issue.1-2, pp.41-68, 2002.
DOI : 10.1016/S0304-3975(00)00347-9
URL : https://hal.archives-ouvertes.fr/inria-00105578

F. Blanqui, Rewriting Modulo in Deduction Modulo, Proc. of the 14th International Conference on Rewriting Techniques and Applications, 2003.
DOI : 10.1007/3-540-44881-0_28
URL : https://hal.archives-ouvertes.fr/inria-00105625

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, issue.1, pp.37-92, 2005.
DOI : 10.1017/S0960129504004426
URL : https://hal.archives-ouvertes.fr/inria-00105568

F. Blanqui, Inductive Types in the Calculus of Algebraic Constructions, Fundamenta Informaticae, vol.65, issue.12, pp.61-86, 2005.
DOI : 10.1007/3-540-44904-3_4
URL : https://hal.archives-ouvertes.fr/inria-00105617

F. Blanqui and C. Riba, Combining typing and size constraints for checking termination of higher-order conditional rewriting systems, Proc. LPAR, to appear in LNAI, 2006.

F. Blanqui, Higher-order dependency pairs, Proceedings of the 8th International Workshop on Termination, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00084821

C. Borralleras and A. Rubio, A Monotonic Higher-Order Semantic Path Ordering, Proceedings LPAR, Lecture Notes in Computer Science, 2006.
DOI : 10.1007/3-540-45653-8_37

V. Breazu-tannen and J. Gallier, Polymorphic rewriting conserves algebraic strong normalization, Theoretical Computer Science, 1990.

A. Podelski, B. Cook, and A. Rybalchenko, Termination proofs for systems code, 2004.

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

N. Dershowitz and J. Jouannaud, Rewrite Systems, pp.243-309, 1990.
DOI : 10.1016/B978-0-444-88074-1.50011-1

N. Jones and N. Bohr, Termination Analysis of the Untyped ??-Calculus, Rewriting techniques and Applications, pp.1-23, 2004.
DOI : 10.1007/978-3-540-25979-4_1

J. and M. Okada, Executable higher-order algebraic specification languages, Proc. 6th IEEE Symp. Logic in Computer Science, pp.350-361, 1991.

J. and M. Okada, Abstract data type systems, Theoretical Computer Science, vol.173, issue.2, pp.349-391, 1997.

J. Jouannaud and A. Rubio, The higher-order recursive path ordering, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782635

J. Jouannaud and A. Rubio, Higher-Order Orderings for Normal Rewriting, Proc. 17th International Conference on Rewriting Techniques and Applications, 2006.
DOI : 10.1007/11805618_29

J. Jouannaud and A. Rubio, Polymorphic higher-order recursive path orderings, Journal of the ACM, vol.54, issue.1
DOI : 10.1145/1206035.1206037

P. Scneider-kamp-jürgen-giesl, S. Swiderski, and R. Thiemann, Automated termination analysis for haskell: Form term rewriting to programming languages, Rewriting techniques and Applications, pp.297-312, 2006.

M. Okada, Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system, Proc. of the 20th Int. Symp. on Symbolic and Algebraic Computation, 1989.

C. Paulin-mohring, Inductive definitions in the system COQ, Typed Lambda Calculi and Applications, pp.328-345, 1993.

M. Sakai and K. Kusakari, On Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems, IEICE Transactions on Information and Systems, vol.88, issue.3, pp.88-583, 2005.
DOI : 10.1093/ietisy/e88-d.3.583

D. Wa?ukiewicz-chrzaszcz, Termination of rewriting in the Calculus of Constructions, Proceedings of the Workshop on Logical Frameworks and Meta-languages, 2000.
DOI : 10.1017/S0956796802004641