T. Altenkirch and A. Kaposi, Type theory in type theory using quotient inductive types, Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages, 2016.

J. Bernardy and M. Lasson, Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures, pp.108-122978, 2011.
DOI : 10.1007/978-3-642-19805-2_8

URL : https://hal.archives-ouvertes.fr/hal-00589893

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01378906

H. Herbelin, A Constructive Proof of Dependent Choice, Compatible with Classical Logic, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.365-374, 2012.
DOI : 10.1109/LICS.2012.47

URL : https://hal.archives-ouvertes.fr/hal-00697240

G. Jaber, N. Tabareau, and M. Sozeau, Extending Type Theory with Forcing, 2012 27th Annual IEEE Symposium on Logic in Computer Science, pp.0-0, 2012.
DOI : 10.1109/LICS.2012.49

URL : https://hal.archives-ouvertes.fr/hal-00685150

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

J. Krivine, Classical logic, storage operators and second-order lambda-calculus, Annals of Pure and Applied Logic, vol.68, issue.1, pp.53-78, 1994.
DOI : 10.1016/0168-0072(94)90047-7

J. Krivine, Realizability in classical logic. Panoramas et synthèses, pp.197-229, 2009.
URL : https://hal.archives-ouvertes.fr/hal-00154500

P. B. Levy, Call-by-push-value, 2001.
DOI : 10.1007/978-94-007-0954-6

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

G. Scherer, Multi-focusing on extensional rewriting with sums, 13th International Conference on Typed Lambda Calculi and Applications Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp.317-331, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01235372

M. Tierney, Sheaf theory and the continuum hypothesis, Toposes, algebraic geometry and logic, pp.13-42, 1972.
DOI : 10.1007/BFb0073963

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