C. Appel, V. Van-oostrom, and J. G. Simonsen, Higher-order (non-)modularity, Proc. RTA 2010, LIPIcs 6, pp.17-32, 2010.

A. Assaf, A calculus of constructions with explicit subtyping, Proc. TYPES 2014, pp.27-46
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf, A framework for defining computational higher-order logics, École Polytechnique, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01235303

A. Assaf and G. Burel, Translating HOL to Dedukti, Proc. PxTP 2015, pp.74-88, 2015.
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

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

M. Boespflug and G. Burel, CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo, Proc. PxTP, p.44, 2012.

M. Clavel, F. Durán, S. Eker, P. Lincoln, N. Martí-oliet et al., All About Maude -A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, LNCS, vol.4350, 2007.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Proc. TLCA 2007, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

H. Goguen, The metatheory of UTT, Proc. TYPES 1994, pp.60-82, 1994.
DOI : 10.1007/3-540-60579-7_4

J. and J. Li, Church-Rosser properties of normal rewriting, Proc. CSL 12, pp.350-365
URL : https://hal.archives-ouvertes.fr/hal-00730271

J. W. Klop, Combinatory reduction systems, 1980.

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

T. Nipkow, Higher-order critical pairs, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.342-349, 1991.
DOI : 10.1109/LICS.1991.151658

U. Norell, Dependently typed programming in Agda, Advanced Functional Programming, 6th International School Revised Lectures, pp.230-266, 2008.

A. Rubio and A. Fully, A Fully Syntactic AC-RPO, Information and Computation, vol.178, issue.2, pp.515-533, 2002.
DOI : 10.1006/inco.2002.3158

M. Sozeau and N. Tabareau, Universe Polymorphism in Coq, Proc. ITP 2014, Vienna Summer of Logic 2014, pp.499-514
DOI : 10.1007/978-3-319-08970-6_32
URL : https://hal.archives-ouvertes.fr/hal-00974721

O. Vincent-van, Confluence by decreasing diagrams, Theor. Comput. Sci, vol.126, issue.2, pp.259-280, 1994.

O. Vincent-van, Developing developments, Theor. Comput. Sci, vol.175, issue.1, pp.159-181, 1997.