J. Arts and . 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

P. Barendregt, Lambda calculus with types In Handbook of Logic in Computer Science, pp.117-309, 1993.

J. Barras, P. Jouannaud, Q. Strub, and . Wang, CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory, 2011 IEEE 26th Annual Symposium on Logic in Computer Science, pp.143-151, 2011.
DOI : 10.1109/LICS.2011.37
URL : https://hal.archives-ouvertes.fr/inria-00583136

. Barthe, The relevance of proof-irrelevance, ICALP, volume 1443 of LNCS, pp.755-768, 1998.
DOI : 10.1007/BFb0055099

. Blanqui, A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, RTA, pp.24-39, 2004.
DOI : 10.1007/978-3-540-25979-4_2
URL : https://hal.archives-ouvertes.fr/inria-00100254

. Blanqui, Definitions by rewriting in the calculus of constructions, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00105648

J. Blanqui, M. Jouannaud, and . Okada, The Calculus of Algebraic Constructions, RTA, volume 1631 of LNCS, pp.301-316, 1999.
DOI : 10.1007/3-540-48685-2_25
URL : https://hal.archives-ouvertes.fr/inria-00105545

J. Blanqui, A. Jouannaud, and . Rubio, HORPO with Computability Closure: A Reconstruction, LPAR, 2007.
DOI : 10.1007/978-3-540-75560-9_12
URL : https://hal.archives-ouvertes.fr/inria-00168304

J. Blanqui, A. Jouannaud, and . Rubio, The Computability Path Ordering: The End of a Quest, CSL, LNCS 5213, 2008.
DOI : 10.1007/978-3-540-87531-4_1
URL : https://hal.archives-ouvertes.fr/inria-00288209

J. Blanqui, A. Jouannaud, and . Rubio, The computability path ordering, Logical Methods in Computer Science, vol.11, issue.4
DOI : 10.2168/LMCS-11(4:3)2015
URL : https://hal.archives-ouvertes.fr/hal-01163091

A. Borralleras and . Rubio, A monotonic higher-order semantic path ordering 12 Nachum Dershowitz. Orderings for term-rewriting systems, LPAR, pp.531-547279, 1982.

F. Harper, G. Honsell, and . Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

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

Y. Kusakari, M. Isogai, F. Sakai, and . Blanqui, Static Dependency Pair Method Based on Strong Computability for Higher-Order Rewrite Systems, IEICE Transactions on Information and Systems, vol.92, issue.10, 1109.
DOI : 10.1587/transinf.E92.D.2007
URL : https://hal.archives-ouvertes.fr/inria-00397820

. Norell, Dependently typed programming in Agda, TLDI, pp.1-2, 2009.

. Paulin-mohring, Inductive definitions in the system Coq rules and properties, TLCA, pp.328-345, 1993.
DOI : 10.1007/BFb0037116

. Pfenning, Elf: a language for logic definition and verified metaprogramming, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pp.313-322, 1989.
DOI : 10.1109/LICS.1989.39186

M. Rondon, M. Kawaguchi, and R. Jhala, Liquid types, PLDI, pp.159-169, 2008.

-. Strub, Coq Modulo Theory, CSL, pp.529-543, 2010.
DOI : 10.1007/978-3-642-15205-4_40
URL : https://hal.archives-ouvertes.fr/inria-00497404

K. Suzuki, F. Kusakari, and . Blanqui, Argument filterings and usable rules in higher-order rewrite systems. CoRR, abs/1109, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00555008

. Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, vol.17, issue.02, pp.215-286, 2007.
DOI : 10.1017/S0956796806006216

F. Xi and . Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.214-227, 1999.
DOI : 10.1145/292540.292560