A. Assaf, A calculus of constructions with explicit subtyping, The 20th International Conference on Types for Proofs and Programs (TYPES '14), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01097401

A. Assaf and &. G. Burel, Translating HOL to Dedukti Available at https, 2014.

F. Blanqui, Termination of rewrite relations on lambda-terms based on Girard's notion of reducibility. Theoretical Computer Science, 2015.

M. Boespflug and &. G. Burel, CoqInE : Translating the calculus of inductive constructions into the ? ?calculus modulo, The Second International Workshop on Proof Exchange for Theorem Proving, 2012.
URL : https://hal.archives-ouvertes.fr/hal-01126128

G. Burel, A Shallow Embedding of Resolution and Superposition Proofs into the ? ?-Calculus Modulo, The Third International Workshop on Proof Exchange for Theorem Proving (PxTP '13), 2013.
URL : https://hal.archives-ouvertes.fr/hal-01126321

R. Cauderlier and &. C. Dubois, Objects and Subtyping in the ? ?-Calculus Modulo, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01126394

D. Cousineau and &. G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, The 8th International Conference on Typed Lambda Calculi and Applications (TLCA '07), 2007.
DOI : 10.1007/978-3-540-73228-0_9

A. Dorra, Equivalence de Curry-Howard entre le lambda-Pi calcul et la logique intuitionniste

H. Geuvers, The Church-Rosser property for beta eta -reduction in typed lambda -calculi, [1992] Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science, 1992.
DOI : 10.1109/LICS.1992.185556

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, 1991.

F. Müller, Confluence of the lambda calculus with left-linear algebraic rewriting, Information Processing Letters, vol.41, issue.6, p.90155, 1992.
DOI : 10.1016/0020-0190(92)90155-O

A. Nanevski, F. Pfenning-&-brigitte, and . Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.
DOI : 10.1145/1352582.1352591

URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796

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

V. Van-oostrom, Development closed critical pairs, 1995.
DOI : 10.1007/3-540-61254-8_26

B. Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Symposium on Principles of Programming Languages, 2008.

R. Saillard, Towards explicit rewrite rules in the ? ?-calculus modulo, The 10th International Workshop on the Implementation of Logics (IWIL '13), 2013.
URL : https://hal.archives-ouvertes.fr/hal-00921340