F. Blanqui, CoLoR, a Coq Library on Rewriting and Termination
URL : https://hal.archives-ouvertes.fr/inria-00084835

A. Chlipala, Certified Programming with Dependent Types, 2013.

H. Eades and &. Stump, Hereditary substitution for stratified system f In: International Workshop on Proof-Search in Type Theories, PSTT, 10, 2010.

H. Goguen, C. Mcbride, and J. Mckinna, Eliminating dependent pattern matching. Algebra, Meaning, and Computation, pp.521-540, 2006.

D. Leivant, Finitely stratified polymorphism, Information and Computation, vol.93, issue.1, 1990.
DOI : 10.1016/0890-5401(91)90053-5

C. Mangin and &. Sozeau, Equations for Hereditary Substitution in Leivant's Predicative System F: A Case Study, Electronic Proceedings in Theoretical Computer Science, vol.185, 2015.
DOI : 10.4204/EPTCS.185.5

M. Sozeau, Equations: A Dependent Pattern-Matching Com- piler Available at http://mattam, First International Conference on Interactive Theorem Proving, 2010.

M. Sozeau, Coq support for HoTT Available at http://www.pps. univ-paris-diderot.fr/ ~ sozeau, 2015.

J. Vouillon, A Solution to the PoplMark Challenge Based on de Bruijn Indices, Journal of Automated Reasoning, vol.40, issue.4, pp.327-362, 2012.
DOI : 10.1007/s10817-011-9230-5
URL : https://hal.archives-ouvertes.fr/hal-00628381