T. Altenkirch and C. Mcbride, Towards observational type theory. Manuscript, available online, 2006.

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, 1991.

E. Brady, C. Mcbride, and J. Mckinna, Inductive Families Need Not Store Their Indices, Types for Proofs and Programs, pp.115-129, 2003.
DOI : 10.1007/978-3-540-24849-1_8

P. Letouzey, Programmation fonctionnelle certifiée ? L'extraction de programmes dans l'assistant Coq, 2004.

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1990.
DOI : 10.1109/LICS.1989.39193

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

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

A. Miquel and B. Werner, The not so simple proofirrelevent model of CC, TYPES, 2002.

S. Owre and N. Shankar, The formal semantics of PVS, 1997.

C. Paulin-mohring and B. Werner, Synthesis of ML programs in the system Coq, Journal of Symbolic Computation, vol.15, issue.5-6, pp.607-640, 1993.
DOI : 10.1016/S0747-7171(06)80007-6

M. Sozeau, Subset Coercions in Coq, postworkshop proceedings of TYPES'2006, 2007.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869

B. Werner, On the Strength of Proof-Irrelevant Type Theories, IJ- CAR, pp.604-618, 2006.
DOI : 10.1007/11814771_49

H. Xi and F. Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '99, pp.214-227, 1999.
DOI : 10.1145/292540.292560
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.548