[. Bishop and D. S. Bridges, Constructive Analysis, volume 279 of Grundlehren der mathematischen Wissenschaften, 1985.

M. Bezem, T. Coquand, S. Huber, and N. Bourbaki, A model of type theory in cubical sets An intuitionistic formula hierarchy based on high-school identities. arXiv:1601.04876, 2016 Foundations of mathematics for the working mathematician Breaking through the normalization barrier: A selfinterpreter for F-omega Self-representation in Girard's system U, 19th International Conference on Types for Proofs and Programs Proceedings of the 43rd Annual ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages. [BP15] Matt Brown and Jens Palsberg Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages Fragments of Heyting arithmetic. The Journal of Symbolic Logic, pp.107-1281, 1949.

E. Bombieri and A. Van-der-poorten, Some quantitative results related to Roth's Theorem, Journal of the Australian Mathematical Society, vol.14, issue.02, pp.233-248, 1988.
DOI : 10.1007/BF01388445

N. Stanley, K. A. Burris, and . Yeats, The saga of the high school identities, Algebra Universalis, vol.52, pp.325-342, 2004.

T. Coquand and P. Dybjer, Intuitionistic model constructions and normalization proofs, Mathematical Structures in Computer Science, vol.7, issue.1, pp.75-94, 1997.
DOI : 10.1017/S0960129596002150

T. Coquand, About Goodman's theorem. Annals of Pure and Applied Logic, pp.437-442, 2013.

T. Coquand, Théorie des types dépendants et axiome d'univalence, Séminaire BOURBAKI, vol.66, p.2014, 1085.

O. Danvy, Type-directed partial evaluation, Proceedings of the Twenty-Third Annual ACM SIGPLAN SIGACT Symposium on Principles of Programming Languages (POPL'96), pp.242-257, 1996.

C. N. Delzell, Kreisel's unwinding of Artin's proof [Do?03] Kosta Do?en. Identity of proofs based on normalization and generality, Kreiseliana. About and Around Georg Kreisel, pp.113-246477, 1996.

M. Fiore, R. D. Cosmo, and V. Balat, Remarks on isomorphisms in typed lambda calculi with empty and sum types, Annals of Pure and Applied Logic, vol.141, issue.1-2, pp.35-50, 2006.
DOI : 10.1016/j.apal.2005.09.001
URL : https://hal.archives-ouvertes.fr/hal-00149560

S. Feferman and . Kreisel, Unwinding " Program A K Peters Makoto Fujiwara, Hajime Ishihara, and Takako Nemoto. Some principles weaker than Markov's principle, Archive for Mathematical Logic, vol.54, issue.78, pp.247-273861, 1996.

H. Friedman, Boolean Relation Theory and Incompleteness. Lecture Notes in Logic, 2015.

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., A Machine-Checked Proof of the Odd Order Theorem, ITP 2013, 4th Conference on Interactive Theorem Proving, pp.163-179, 2013.
DOI : 10.1007/978-3-642-39634-2_14
URL : https://hal.archives-ouvertes.fr/hal-00816699

J. Gonthier, Proof theory and logical complexity Formal proof?the four-color theorem. Notices of the AMS A new proof of Szemerédi's theorem, Bibliopolis Geometric & Functional Analysis GAFA, vol.1, issue.113, pp.1382-1393465, 1987.

G. Timothy, B. Griffin, T. Green, ]. R. Taogur90, and . Gurevi?, A formula-as-types notion of control The primes contain arbitrarily long arithmetic progressions Equational theory of positive numbers with exponentiation is not finitely axiomatizable, Conf. Record 17th Annual ACM Symp. on Principles of Programming Languages, POPL'90 Annals of Pure and Applied Logic, pp.17-19, 1990.

T. Hales, Dense sphere packings: A blueprint for formal proofs Lecture Note Series, 2012.
DOI : 10.1017/CBO9781139193894

G. Harold and H. , Orders of Infinity. The 'Infinitärcalcül' of Paul Du Bois- Reymond. Cambridge Tracts in Mathematic and Mathematical Physics, 1910.

H. Herbelin, An Intuitionistic Logic that Proves Markov's Principle, 2010 25th Annual IEEE Symposium on Logic in Computer Science, pp.11-14
DOI : 10.1109/LICS.2010.49

M. Hofmann and T. Streicher, The groupoid interpretation of type theory In Twenty-five years of constructive type theory, Oxford Logic Guides, vol.36, pp.83-111, 1995.

D. Ilik, Constructive Completeness Proofs and Delimited Control, 2010.
URL : https://hal.archives-ouvertes.fr/tel-00529021

D. Ilik, Delimited control operators prove Double-negation Shift, Annals of Pure and Applied Logic, vol.163, issue.11, pp.1549-1559, 2012.
DOI : 10.1016/j.apal.2011.12.008
URL : https://hal.archives-ouvertes.fr/hal-00647389

D. Ilik, Continuation-passing style models complete for intuitionistic logic, Annals of Pure and Applied Logic, vol.164, issue.6, pp.651-662, 2013.
DOI : 10.1016/j.apal.2012.05.003
URL : https://hal.archives-ouvertes.fr/hal-00647390

D. Ilik, Type Directed Partial Evaluation for Level-1 Shift and Reset, Proceedings First Workshop on Control Operators and their Semantics of Electronic Proceedings in Theoretical Computer Science, pp.86-100, 2013.
DOI : 10.4204/EPTCS.127.6

D. Ilik, An interpretation of the Sigma-2 fragment of classical Analysis in System T, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01092411

D. Ilik, Axioms and decidability for type isomorphism in the presence of sums, Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS '14, pp.1-537, 2014.
DOI : 10.1145/2603088.2603115
URL : https://hal.archives-ouvertes.fr/hal-00991147

D. Ilik, On the exp-log normal form of types, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01167162

D. Ilik, K. Nakata, and V. Voevodsky, A direct version of Veldman's proof of open induction on Cantor space via delimited control operators The simplicial model of univalent foundations. arXiv preprint, Leibniz International Proceedings in Informatics (LIPIcs), pp.188-201, 2012.

G. Kreisel and A. Macintyre, Constructive logic versus algebraization I [Koh93] Ulrich Kohlenbach. New effective moduli of uniqueness and uniform a priori estimates for constants of strong unicity by logical analysis of known proofs in best approximation theory. Numerical Functional Analysis and Optimization A note on Goodman's theorem, Koh05] Ulrich Kohlenbach. Some logical metatheorems with applications in functional analysis . Transactions of the, pp.217-260581, 1982.

G. Kreisel, On the interpretation of non-finitist proofs?Part I. The Journal of Symbolic Logic, pp.241-267, 1951.

G. Kreisel, Mathematical significance of consistency proofs. The Journal of Symbolic Logic, pp.155-182, 1958.

G. Kreisel, Interpretation of analysis by means of constructive functionals of finite types Proceedings of the colloqium held at Amsterdam, 1957, Studies in Logic and The Foundations of Mathematics, Constructivity in Mathematics, pp.101-127, 1959.

J. Krivine, On the structure of classical realizability models of ZF

H. Lombardi and C. Quitté, Algèbre commutative ? Méthodes constructives, Calvage & Mounet, 2011.

H. Luckhardt, Abstract, The Journal of Symbolic Logic, vol.5, issue.269, pp.234-263, 1989.
DOI : 10.1007/BF01388644

H. Luckhardt, Bounds Extracted by Kreisel From Ineffective Proofs, Kreiseliana. About and Around Georg Kreisel, pp.289-300, 1996.

A. Macintyre, The laws of exponentiation, Lecture Notes in Mathematics, vol.15, pp.185-197, 1981.
DOI : 10.1002/malq.19690152003

A. Macintyre, The mathematical significance of proof theory, Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol.92, issue.1835, pp.2419-2435147, 1835.
DOI : 10.1098/rsta.2005.1656

J. Paris and L. Harrington, A mathematical incompleteness in Peano arithmetic. Handbook of mathematical logic, pp.1133-1142, 1977.

D. Richardson, Solution of the identity problem for integral exponential functions, Zeitschrift für mathematische Logik und Grundlagen der Mathematik, pp.333-340, 1969.
DOI : 10.1002/malq.19690152003

M. Rittri, Abstract, Journal of Functional Programming, vol.19, issue.01, pp.71-89, 1991.
DOI : 10.1016/S0747-7171(89)80012-4

M. Raussen and C. Skau, Interview with Abel laureate John F On bar recursion of types 0 and 1, Nash Jr. European Mathematical Society. Newsletter The Journal of Symbolic Logic, vol.97, issue.3, pp.26-31, 1979.

P. Schuster, Induction in algebra: A first case study, Logical Methods in Computer Science, vol.9, issue.3, pp.1-19, 2013.

[. Schwichtenberg and S. S. Wainer, Proofs and Computations. Perspectives in Logic, 2012.

E. Szemerédi, On sets of integers containing no four elements in arithmetic progression, Acta Mathematica Academiae Scientiarum Hungaricae, vol.20, issue.1-2, pp.199-245, 1975.
DOI : 10.1007/BF01894569

R. Thiele, Hilbert's twenty-fourth problem [Uni13] The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, American Mathematical Monthly, 2003.

W. Veldman, An intuitionistic proof of Kruskal's theorem. Archive for Mathematical Logic, pp.215-264, 2001.

W. Veldman, The principle of open induction on Cantor space and the approximatefan theorem

A. Weiermann, Analytic combinatorics, proof-theoretic ordinals, and phase transitions for independence results, Annals of Pure and Applied Logic, vol.136, issue.1-2, 2005.
DOI : 10.1016/j.apal.2005.05.012

A. Wilkie, On exponentiation ? a solution to Tarski's high school algebra problem, Quaderni di Matematica, vol.6, 2000.