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, Conservativity of embeddings in the lambda pi calculus modulo rewriting, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, pp.31-44, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01084165

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

F. Blanqui, J. Jouannaud, and M. Okada, The Calculus of Algebraic Constructions, Proceedings of the 9th International Conference on Rewriting Techniques and Applications (RTA '99), number 1631 in LNCS, pp.301-316, 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

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.

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

J. Jouannaud and C. Kop, Church-rosser properties of terminating rewriting computations

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. Liu, J. Jouannaud, and M. Ogawa, Confluence of layered rewrite systems, 24th EACSL Annual Conference on Computer Science Logic, CSL 2015 Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.423-440, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01199062

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

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.