C. Appel, V. Van-oostrom, and J. G. Simonsen, Higher-order (non-)modularity, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.17-32, 2010.

A. Assaf, A calculus of constructions with explicit subtyping, 20th International Conference on Types for Proofs and Programs, TYPES 2014 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.27-46, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01097401

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

A. Assaf and G. Burel, Translating HOL to Dedukti, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, pp.74-88, 2015.
DOI : 10.4204/EPTCS.186.8
URL : https://hal.archives-ouvertes.fr/hal-01097412

H. P. Barendregt, The lambda calculus : its syntax and semantics. Studies in logic and the foundations of mathematics, 1981.

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, Termination of rewrite relations on ??-terms based on Girard's notion of reducibility, Theoretical Computer Science, vol.611, pp.50-86, 2016.
DOI : 10.1016/j.tcs.2015.07.045

M. Boespflug and G. Burel, CoqInE: Translating the calculus of inductive constructions into the lambda-Pi-calculus modulo, Proof Exchange for Theorem Proving?Second International Workshop, p.44, 2012.

A. Boudet and E. Contejean, AC-unification of higher-order patterns, Int. Conf. on Constraint Programming, pp.267-281, 1997.
DOI : 10.1007/BFb0017445
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.67

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, Lecture Notes in Computer Science, vol.4350, 2007.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference Proceedings, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

H. Goguen, The metatheory of UTT, Types for Proofs and Programs, International Workshop TYPES'94, pp.60-82, 1994.
DOI : 10.1007/3-540-60579-7_4

G. Huet, Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems: Abstract Properties and Applications to Term Rewriting Systems, Journal of the ACM, vol.27, issue.4, pp.797-821, 1980.
DOI : 10.1145/322217.322230

J. Jouannaud and H. Kirchner, Completion of a Set of Rules Modulo a Set of Equations, SIAM Journal on Computing, vol.15, issue.4, pp.1155-1194, 1986.
DOI : 10.1137/0215084

J. Jouannaud and C. Marché, Termination and completion modulo associativity, commutativity and identity, Theoretical Computer Science, vol.104, issue.1, pp.29-51, 1992.
DOI : 10.1016/0304-3975(92)90165-C
URL : http://doi.org/10.1016/0304-3975(92)90165-c

J. and J. Li, Church-Rosser properties of normal rewriting Computer Science Logic (CSL'12) -21st Annual Conference of the EACSL, CSL 2012, Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.350-365, 2012.

J. and J. Liu, From diagrammatic confluence to modularity, Theor. Comput. Sci, vol.464, pp.20-34, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730272

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

S. Lucas and J. Meseguer, Normal forms and normal theories in conditional rewriting, Journal of Logical and Algebraic Methods in Programming, vol.85, issue.1, pp.67-97, 2016.
DOI : 10.1016/j.jlamp.2015.06.001

C. Marché, Normalized Rewriting: an Alternative to Rewriting modulo a Set of Equations, Journal of Symbolic Computation, vol.21, issue.3, pp.253-288, 1996.
DOI : 10.1006/jsco.1996.0011

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
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.160.8728

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, pp.230-266, 2008.
DOI : 10.1017/S0956796803004829
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.2234

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, Interactive Theorem Proving -5th International Conference Proceedings, pp.499-514, 2014.
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.

O. Vincent-van, Confluence by decreasing diagrams converted, Lecture Notes in Computer Science, vol.5117, pp.306-320, 2008.