A. Abel, J. Öhman, and A. Vezzosi, Decidability of Conversion for Type Theory in Type Theory, Proceedings of the ACM on Programming Languages 2, POPL, vol.29, p.23, 2018.

A. Abel and B. Pientka, Higher-Order Dynamic Pattern Unification for Dependent Types and Records, Typed Lambda Calculi and Applications -10th International Conference, vol.6690, pp.10-26, 2011.

C. /-guillaume-allais, P. Mcbride, and . Boutillier, New Equations for Neutral Terms: A Sound and Complete Decision Procedure, Formalized, Proceedings of the 2013 ACM SIGPLAN Workshop on Dependently-typed Programming (DTP '13), pp.13-24, 2013.

C. Appel, J. G. Vincent-van-oostrom, and . Simonsen, Higher-Order (Non-)Modularity, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, vol.6, pp.17-32, 2010.

A. Assaf and G. Burel, Translating HOL to Dedukti, Electronic Proceedings in Theoretical Computer Science, vol.186, pp.74-88, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01097412

F. Barbanera, M. Fernández, and H. Geuvers, Modularity of Strong Normalization in the Algebraiclambda-Cube, Journal of Functional Programming, vol.7, pp.613-660, 1997.

H. Barendregt, The Lambda Calculus, Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol.103, 1984.

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

U. Berger, R. Matthes, and A. Setzer, Martin Hofmann's Case for Non-Strictly Positive Data Types, 24th International Conference on Types for Proofs and Programs, vol.130, pp.1-1, 2018.

F. Blanqui, A Type-Based Termination Criterion for Dependently-Typed Higher-Order Rewrite Systems, Rewriting Techniques and Applications, 15th International Conference, vol.3091, pp.24-39, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00100254

F. Blanqui, Definitions by rewriting in the Calculus of Constructions, Mathematical Structures in Computer Science, vol.15, pp.37-92, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00105648

F. Blanqui, Size-based termination of higher-order rewriting, Journal of Functional Programming, vol.28, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01424921

F. Blanqui, Type Safety of Rewrite Rules in Dependent Types, 5th International Conference on Formal Structures for Computation and Deduction, vol.2020, pp.1-13, 2020.

F. Blanqui, J. Jouannaud, and A. Rubio, The Computability Path Ordering: The End of a Quest, Computer Science Logic, 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, vol.5213, pp.1-14, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00288209

M. Boespflug, Q. Carbonneaux, and O. Hermant, The ??-calculus Modulo as a Universal Proof Language, the Second International Workshop on Proof Exchange for Theorem Proving, vol.878, pp.28-43, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00917845

J. Chrzaszcz and D. Walukiewicz-chrzaszcz, Towards Rewriting in Coq, Rewriting, Computation and Proof, Essays Dedicated to Jean-Pierre Jouannaud on the Occasion of His 60th Birthday, vol.4600, pp.113-131, 2007.

J. Cockx, Type theory unchained: Extending Agda with user-defined rewrite rules (system description), 2020.

, The Coq proof assistant reference manual, 2016.

T. Coquand and C. Paulin, Inductively Defined Types, Proceedings of the International Conference on Computer Logic (COLOG '88), pp.50-66, 1988.

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 8th International Conference, vol.4583, pp.102-117, 2007.

B. Felgenhauer and . Vincent-van-oostrom, Proof Orders for Decreasing Diagrams, 24th International Conference on Rewriting Techniques and Applications, RTA 2013, vol.21, pp.174-189, 2013.

G. Ferey and J. Jouannaud, Confluence in (Un)Typed Higher-Order Theories by means of Critical Pairs, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02096540

G. Genestier, SizeChangeTool: A Termination Checker for Rewriting Dependent Types, HOR 2019 -10th International Workshop on Higher-Order Rewriting (Joint Proceedings of HOR 2019 and IWC 2019), pp.14-19, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02442465

G. Gilbert, J. Cockx, M. Sozeau, and N. Tabareau, Definitional Proof-Irrelevance without K, Proceedings of the ACM on Programming Languages, vol.3, pp.1-28, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01859964

M. Hofmann, Non Strictly Positive Datatypes in System F. Email on types mailing list, 1993.

J. and J. Li, Termination of Dependently Typed Rewrite Rules, 13th International Conference on Typed Lambda Calculi and Applications, vol.38, pp.257-272, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01239083

J. and M. Okada, A Computation Model for Executable Higher-Order Algebraic Specification Languages, Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, pp.350-361, 1991.

J. and A. Rubio, The Higher-Order Recursive Path Ordering, Proceedings, 14th Annual IEEE Symposium on Logic in Computer Science, pp.402-411, 1999.

J. and P. Strub, Coq without Type Casts: A Complete Proof of Coq Modulo Theory, LPAR-21: 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EasyChair, pp.474-489, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01664457

N. D. Chin-soon-lee, A. M. Jones, and . Ben-amram, The size-change principle for program termination, Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.81-92, 2001.

J. Liu, Confluence properties of rewrite rules by decreasing diagrams. (Propriétés de confluence des règles de réécriture par des diagrammes décroissants), 2016.
URL : https://hal.archives-ouvertes.fr/tel-01515698

P. Martin-löf, An Intuitionistic Theory of Types: Predicative Part, Studies in Logic and the Foundations of Mathematics, vol.80, pp.71945-71946, 1975.

C. Paulin-mohring, Introduction to the Calculus of Inductive Constructions, Studies in Logic (Mathematical logic and foundations), vol.55, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01094195

P. , M. Pédrot, and N. Tabareau, Failure is Not an Option: An Exceptional Type Theory, ESOP 2018 -27th European Symposium on Programming, vol.10801, pp.245-271, 2018.

P. Pédrot, N. Tabareau, H. J. Fehrmann, and É. Tanter, A Reasonably Exceptional Type Theory, Proceedings of the ACM on Programming Languages 3, ICFP, Article, vol.108, 2019.

R. Saillard, Typechecking in the lambda-Pi-Calculus Modulo: Theory and Practice, Ph.D. Dissertation. MINES ParisTech, 2015.
URL : https://hal.archives-ouvertes.fr/tel-01299180

G. Smolka, Confluence and Normalization in Reduction Systems, 2015.

M. Sozeau, A. Anand, S. Boulier, C. Cohen, Y. Forster et al., The MetaCoq Project, Journal of Automated Reasoning, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02167423

M. Sozeau, S. Boulier, Y. Forster, N. Tabareau, and T. Winterhalter, Coq Coq Correct! Verification of Type Checking and Erasure for Coq, Coq. Proceedings of the ACM on Programming Languages 4, POPL, Article, vol.8, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02380196

M. Stehr, The Open Calculus of Constructions (Part I): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving, Fundamenta Informaticae, vol.68, pp.131-174, 2005.

M. Stehr, The Open Calculus of Constructions (Part II): An Equational Type Theory with Dependent Types for Programming, Specification, and Interactive Theorem Proving, Fundamenta Informaticae, vol.68, pp.249-288, 2005.

P. Strub, Coq Modulo Theory, Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL, vol.6247, pp.529-543, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00497404

M. Takahashi, Parallel Reductions in ?-Calculus, Information and Computation, vol.118, pp.120-127, 1995.

V. Tannen, Combining Algebra and Higher-Order Types, Proceedings, Third Annual Symposium on Logic in Computer Science, pp.82-90, 1988.

T. , Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol.55, 2003.

, The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study

. Vincent-van-oostrom, Confluence by Decreasing Diagrams, Theoretical Computer Science, vol.126, pp.259-280, 1994.

. Vincent-van-oostrom, Confluence for abstract and higher-order rewriting, 1994.

. Vincent-van-oostrom, Selected Papers (Lecture Notes in Computer Science), Gilles Dowek, Higher-Order Algebra, Logic, and Term Rewriting, Second International Workshop, HOA '95, vol.1074, pp.185-200, 1995.

D. Walukiewicz-chrzaszcz, Termination of rewriting in the Calculus of Constructions, Journal of Functional Programming, vol.13, pp.339-414, 2003.

D. Walukiewicz, -. , and J. Chrzaszcz, Consistency and Completeness of Rewriting in the Calculus of Constructions, Automated Reasoning, Third International Joint Conference, vol.4130, pp.619-631, 2006.