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.
DOI : 10.1017/cbo9781139032636

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