A. W. Appel, P. Mellì-es, C. D. Richards, and J. Vouillon, A very modal model of a modern, major, general type system, Proceedings of POPL'07, 2007.
URL : https://hal.archives-ouvertes.fr/hal-00150978

L. Birkedal, R. Møgelberg, J. Schwinghammer, and K. Støvring, First steps in synthetic guarded domain theory: step-indexing in the topos of trees, Proceedings of LICS'11, 2011.

L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg et al., Step-indexed Kripke models over recursive worlds, Proceedings of POPL'11, 2011.

P. J. Cohen and M. Davis, Set theory and the continuum hypothesis, 1966.

D. Dreyer, G. Neis, and L. Birkedal, The impact of higherorder state and control effects on local relational reasoning, Proceedings of ICFP'10, 2010.

M. Hofmann, Extensional concepts in intensional type theory, 1995.
DOI : 10.1007/978-1-4471-0963-1

T. J. Jech, Set theory, 2003.
DOI : 10.1007/978-3-662-22400-7

J. L. Krivine, Realizability algebras: a program to well order R, Logical Methods in Computer Science, vol.7, issue.3, 2011.
DOI : 10.2168/LMCS-7(3:2)2011

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

A. M. Levin, One conservative extension of formal mathematic analysis with a scheme of dependent choice, Mathematical Notes of the Academy of Sciences of the USSR, vol.75, issue.No. 3, pp.524-528, 1977.
DOI : 10.1007/BF01147693

S. , M. Lane, and I. Moerdijk, Sheaves in geometry and logic: A first introduction to topos theory, 1992.

N. Oury, Extensionality in the Calculus of Constructions, Theorem Proving in Higher Order Logics, pp.278-293, 2005.
DOI : 10.1007/11541868_18

A. M. Pitts and I. D. Stark, Operational reasoning for functions with local state, Higher Order Operational Techniques in Semantics. CUP, 1998.

M. Sozeau, An environment for programming with dependent types, 2008.

M. Tierney, Sheaf theory and the continuum hypothesis, LNM, vol.274, pp.13-42, 1972.
DOI : 10.1007/BFb0073963