A. Abel, Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation thesis, 2013.

A. Abel and T. Coquand, Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality, 2019.

A. Abel and C. Sattler, Normalization by Evaluation for Call-By-Push-Value and Polarized Lambda Calculus, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, 2019.

T. A. , Extensional Equality in Intensional Type Theory, 14th Annual IEEE Symposium on Logic in Computer Science, pp.412-420, 1999.

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

J. Avigad and S. Feferman, The Handbook of Proof Theory, Chapter Gödel's functional, pp.337-405, 1999.

F. Barral, Decidability for non-standard conversions in typed lambda-calculi, 2008.

M. Beeson, Foundations of Constructive Mathematics: Metamathematical Studies. Number 6 in Ergebnisse der Mathematik und ihrer Grenzgebiete, 1985.

J. Bernardy, T. Coquand, and G. Moulin, A Presheaf Model of Parametric Type Theory, Electr. Notes Theor. Comput. Sci, vol.319, pp.67-82, 2015.

J. , P. Bernardy, and M. Lasson, Realizability and Parametricity in Pure Type Systems, Foundations of Software Science and Computational Structures, vol.6604, pp.108-122, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00589893

A. Bizjak, R. Hans-bugge-grathwohl, and . Clouston, Guarded Dependent Type Theory with Coinductive Types, Foundations of Software Science and Computation Structures -19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, pp.20-35, 2016.

S. P. Boulier, Extending type theory with syntactic models. (Etendre la théorie des types à l'aide de modèles syntaxiques). Ph.D. Dissertation. Ecole nationale supérieure Mines-Télécom Atlantique Bretagne Pays de la Loire, 2018.
URL : https://hal.archives-ouvertes.fr/tel-02007839

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom, FLAP, vol.4, pp.3127-3170, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01378906

. Thierry-coquand, Canonicity and normalization for dependent type theory, Theor. Comput. Sci, vol.777, pp.184-191, 2019.

T. Coquand and M. Hofmann, A new method for establishing conservativity of classical systems over their intuitionistic version, Mathematical Structures in Computer Science, vol.9, pp.323-333, 1999.

T. Coquand, S. Huber, and C. Sattler, Homotopy Canonicity for Cubical Type Theory, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, vol.11, pp.1-11, 2019.

T. Coquand and B. Mannaa, The Independence of Markov's Principle in Type Theory, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, vol.17, pp.1-17, 2016.

P. Dagand, L. Rieg, and G. Scherer, Dependent Pearl: Normalization by realizability, 2019.

M. Dummett, Elements of Intuitionism, 1977.

H. Friedman, Classically and intuitionistically provably recursive functions, pp.21-27, 1978.

C. Führmann, Direct Models for the Computational Lambda Calculus, Electr. Notes Theor. Comput. Sci, vol.20, pp.245-292, 1999.

G. Gilbert, A type theory with definitional proofirrelevance, 2019.

G. Gilbert, J. Cockx, M. Sozeau, and N. Tabareau, Definitional proof-irrelevance without K, PACMPL, vol.3, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01859964

D. Gratzer, J. Sterling, and L. Birkedal, Implementing a modal dependent type theory, PACMPL, vol.3, pp.1-107, 2019.

H. Herbelin, An Intuitionistic Logic that Proves Markov's Principle, Proceedings of the 25th Annual Symposium on Logic in Computer Science, LICS 2010, pp.50-56, 2010.

H. Herbelin and S. Ghilezan, An approach to callby-name delimited continuations, Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.383-394, 2008.

M. Hofmann, Extensional constructs in intensional type theory, 1997.

S. Huber, Canonicity for Cubical Type Theory, J. Autom. Reasoning, vol.63, pp.173-210, 2019.

. Danko-ilik, Constructive Completeness Proofs and Delimited Control, 2010.

. D. Ph, . Dissertation, and . École-polytechnique,

. Danko-ilik, Continuation-passing style models complete for intuitionistic logic, Ann. Pure Appl. Logic, vol.164, pp.651-662, 2013.

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

G. Jaber, N. Tabareau, and M. Sozeau, Extending Type Theory with Forcing, Proceedings of the 27th, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00685150

, Annual IEEE Symposium on Logic in Computer Science, LICS 2012, pp.395-404, 2012.

A. Kaposi, S. Huber, and C. Sattler, Gluing for Type Theory, 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, vol.25, pp.1-25, 2019.

. Stephen-cole-kleene, On the Interpretation of Intuitionistic Number Theory, J. Symb. Log, vol.10, pp.109-124, 1945.

U. Kohlenbach, Applied Proof Theory -Proof Interpretations and their Use in Mathematics, 2008.

G. Kreisel, On Weak Completeness of Intuitionistic Predicate Logic, J. Symb. Log, vol.27, pp.139-158, 1962.

J. Krivine, Classical Logic, Storage Operators and Second-Order lambda-Calculus, Ann. Pure Appl. Logic, vol.68, pp.90047-90054, 1994.

C. Mccarty, Constructivism in Mathematics, Philosophy of mathematics, pp.311-343, 2009.

A. Miquel, Forcing as a Program Transformation, Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, pp.197-206, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00800558

P. , M. Pédrot, and N. Tabareau, Failure is Not an Option -An Exceptional Type Theory, Programming Languages and Systems -27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, vol.10801, pp.245-271, 2018.

P. , M. Pédrot, and N. Tabareau, The Fire Triangle, Proceedings of the 47st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '20), 2020.

V. Rahli and M. Bickford, Validating Brouwer's continuity principle for numbers using named exceptions, Mathematical Structures in Computer Science, vol.28, pp.942-990, 2018.

J. Sterling and B. Spitters, Normalization by gluing for free -theories, 2018.

, Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, 1973.

, The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics

C. Xu, Sheaf models of type theory in type theory, 2016.