T. Altenkirch, Extensional equality in intensional type theory, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), 1999.
DOI : 10.1109/LICS.1999.782636

T. Altenkirch and A. Kaposi, Type theory in type theory using quotient inductive types, Proceedings of POPL, 2016.

J. Bernardy and M. Lasson, Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures, pp.108-122, 2011.
DOI : 10.1007/978-3-642-19805-2_8
URL : https://hal.archives-ouvertes.fr/hal-00589893

J. Bernardy and G. Moulin, A Computational Interpretation of Parametricity, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.25

J. Bernardy, P. Jansson, and R. Paterson, Parametricity and dependent types, Proceedings of ICFP, 2010.
DOI : 10.1145/1932681.1863592
URL : http://openaccess.city.ac.uk/13223/1/pts.pdf

J. Chapman, Type Theory Should Eat Itself, Electronic Notes in Theoretical Computer Science, vol.228, pp.21-36, 2009.
DOI : 10.1016/j.entcs.2008.12.114
URL : http://doi.org/10.1016/j.entcs.2008.12.114

P. Dybjer, Internal type theory, Types for Proofs and Programs, pp.120-134, 1996.
DOI : 10.1007/3-540-61780-9_66

P. Dybjer, Abstract, The Journal of Symbolic Logic, vol.49, issue.02, pp.525-549, 2000.
DOI : 10.1017/CBO9780511569807.011

M. Hoffman, Syntax and semantics of dependent types, Semantics and Logics of Computation, pp.241-298, 1997.

M. Hofmann, Extensional constructs in intensional type theory. CPHC/BCS distinguished dissertations, 1997.

G. Jaber, N. Tabareau, and M. Sozeau, Extending Type Theory with Forcing, 2012 27th Annual IEEE Symposium on Logic in Computer Science, 2012.
DOI : 10.1109/LICS.2012.49
URL : https://hal.archives-ouvertes.fr/hal-00685150

G. Jaber, G. Lewertoski, P. Pédrot, N. Tabareau, and M. Sozeau, The Definitional Side of the Forcing, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, 2016.
DOI : 10.1145/2933575.2935320
URL : https://hal.archives-ouvertes.fr/hal-01319066

B. Jacobs, Comprehension categories and the semantics of type dependency, Theoretical Computer Science, vol.107, issue.2, pp.169-207, 1993.
DOI : 10.1016/0304-3975(93)90169-T

C. Kapulkin, P. L. Lumsdaine, and V. Voevodsky, The simplicial model of univalent foundations, 2012.

Y. Lafont, B. Reus, and T. Streicher, Continuation semantics or expressing implication by negation, 1993.

Z. Luo, ECC, an extended calculus of constructions, [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, 1989.
DOI : 10.1109/LICS.1989.39193
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.7596

C. Paulin-mohring, Extraction de programmes dans le Calcul des Constructions, Thèse d'université, 1989.
URL : https://hal.archives-ouvertes.fr/tel-00431825

V. Siles and H. Herbelin, Pure Type System conversion is always typable, Journal of Functional Programming, vol.1, issue.02, pp.153-180, 2012.
DOI : 10.1017/S0956796805005770
URL : https://hal.archives-ouvertes.fr/inria-00497177

C. The and . Team, The Coq proof assistant reference manual, 2015.

B. Werner, Sets in types, types in sets, Theoretical aspects of computer software, pp.530-546, 1997.
DOI : 10.1007/BFb0014566