T. Coquand, Pattern matching with dependent types, Informal Proceedings Workshop on Types for Proofs and Programs, 1992.

H. Goguen, C. Mcbride, and J. Mckinna, Eliminating Dependent Pattern Matching, Essays Dedicated to J. Goguen, 2006.
DOI : 10.1007/11780274_27
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.101.7522

M. Hofmann and T. Streicher, The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, pp.208-212, 1994.
DOI : 10.1109/LICS.1994.316071

C. Mcbride, Dependently Typed Functional Programs and their Proofs, 1999.

C. Mcbride, Epigram: Practical Programming with Dependent Types, LNCS, vol.3622, 2004.
DOI : 10.1007/11546382_3

C. Mcbride and J. Mckinna, The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004.
DOI : 10.1017/S0956796803004829

U. Norell, Towards a practical programming language based on dependent type theory, 2007.

N. Oury, Pattern matching coverage checking with dependent types using set approximations, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.47-56, 2007.
DOI : 10.1145/1292597.1292606

C. Paulin-mohring, Inductive definitions in the system Coq rules and properties, TLCA '93, 1993.
DOI : 10.1007/BFb0037116

C. Schürmann and F. Pfenning, A Coverage Checking Algorithm for LF, TPHOLs '03, pp.120-135, 2003.
DOI : 10.1007/10930755_8

M. Sozeau, Subset Coercions in Coq, LNCS, vol.4502, pp.237-252, 2006.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869

B. Werner, Une Théorie des Constructions Inductives, 1994.