J. Avigad and V. Brattka, Computability and analysis: the legacy of Alan Turing, Lecture Notes in Logic, pp.1-47, 2014.

R. Affeldt, C. Cohen, and D. Rouhling, Formalization techniques for asymptotic reasoning in classical analysis, Journal of Formalized Reasoning, vol.11, issue.1, pp.43-76, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01719918

K. Ambos-spies, U. Brandt, and M. Ziegler, Real benefit of promises and advice, The Nature of Computation. Logic, Algorithms, Applications, pp.1-11, 2013.

A. Bauer, The Realizability Approach to Computable Analysis and Topology, 2000.

E. Bishop and D. Bridges, Constructive analysis, vol.279, 2012.

F. Sylvie-boldo, J. Clément, M. Filliâtre, G. Mayero, P. Melquiond et al., Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.50, issue.4, pp.423-456, 2013.

S. Boldo, F. Clément, F. Faissole, V. Martin, and M. Mayero, A Coq Formal Proof of the Lax-Milgram theorem, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.79-89, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01391578

V. Brattka, M. D. Brecht, and A. Pauly, Closed choice and a uniform low basis theorem, Annals of Pure and Applied Logic, vol.163, issue.8, pp.986-1008, 2012.

V. Brattka and G. Gherardi, Effective choice and boundedness principles in computable analysis, Bulletin of Symbolic Logic, vol.17, issue.1, pp.73-117, 2011.

V. Brattka, G. Gherardi, and A. Pauly, Weihrauch complexity in computable analysis, 2017.

V. Brattka, A. Kawamura, A. Marcone, and A. Pauly, Measuring the Complexity of Computational Content (Dagstuhl Seminar 15392)

, Dagstuhl Reports, vol.5, issue.9, pp.77-104, 2016.

J. Blanck, Exact real arithmetic systems: Results of competition, Computability and complexity in analysis. 4th international workshop, CCA, pp.389-393, 2000.

S. Boldo, C. Lelay, and G. Melquiond, Coquelicot: A userfriendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015.
URL : https://hal.archives-ouvertes.fr/hal-00860648

S. Boldo, C. Lelay, and G. Melquiond, Formalization of real analysis: A survey of proof assistants and libraries, Mathematical Structures in Computer Science, vol.26, issue.7, pp.1196-1233, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00806920

S. Boldo and G. Melquiond, Computer Arithmetic and Formal Proofs, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632617

Y. Bertot, L. Rideau, and L. Théry, Distant decimals of ?, Journal of Automated Reasoning, pp.1-45, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01582524

A. Bauer and C. A. Stone, RZ: A tool for bringing constructive and computable mathematics closer to programming practice. Computation and Logic in the Real World, Lecture Notes in Computer Science, vol.4497, 2007.

L. Blum, M. Shub, and S. Smale, On a theory of computation and complexity over the real numbers: NP-completeness, recursive functions and universal machines, Bulletin of the American Mathematical Society, vol.21, issue.1, pp.1-46, 1989.

V. Brattka and A. Yoshikawa, Towards computability of elliptic boundary value problems in variational formulation, Computability and Complexity in Analysis, vol.22, issue.6, pp.858-880, 2006.

L. Cruz-filipe, H. Geuvers, and F. Wiedijk, C-CoRN, the constructive Coq repository at Nijmegen, International Conference on Mathematical Knowledge Management, pp.88-103, 2004.

C. Cohen, Construction of real algebraic numbers in Coq, ITP -3rd International Conference on Interactive Theorem Proving -2012, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00671809

C. Cohen, Pragmatic quotient types in coq, Interactive Theorem Proving, pp.213-228, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01966714

K. Deimling, Multivalued Differential Equations. De Gruyter series in nonlinear analysis and applications, 1992.

S. Eilenberg and D. Montgomery, Fixed point theorems for multi-valued transformations, American Journal of Mathematics, vol.68, issue.2, pp.214-222, 1946.
DOI : 10.2307/2371832

M. Escardó and C. Xu, A constructive manifestation of the Kleene-Kreisel continuous functionals, Fourth Workshop on Formal Topology (4WFTop), vol.167, pp.770-793, 2016.

H. Feree, Game semantics approach to higher-order complexity, J. Comput. Syst. Sci, vol.87, issue.C, pp.1-15, 2017.

H. Férée, S. Hym, M. Mayero, J. Moyen, and D. Nowak, Formal proof of polynomial-time complexity with quasi-interpretations, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp.146-157, 2018.

Y. Forster and G. Smolka, Call-by-Value Lambda Calculus as a Model of Computation in Coq, Journal of Automated Reasoning, 2018.

A. Grzegorczyk, On the definitions of computable real continuous functions, Fund. Math, vol.44, pp.61-71, 1957.

F. Immler and J. Hölzl, Numerical analysis of ordinary differential equations in Isabelle/HOL, ITP, vol.7406, pp.377-392, 2012.

M. Bruce, S. A. Kapron, and . Cook, A new characterization of type-2 feasibility, SIAM J. Comput, vol.25, pp.117-132, 1996.

A. Kawamura and S. Cook, Complexity theory for operators in analysis, ACM Transactions in Computation Theory, vol.4, issue.2, 2012.

S. C. Kleene, Countable functionals. Constructivity in Mathematics: proceedings of the colloquium held at Amsterdam, 1959.

M. Konecn´ykonecn´y and E. Neumann, Representations and evaluation strategies for feasibly approximable functions, 2017.

-. Ker and . Ko, Complexity theory of real functions. Progress in Theoretical Computer Science, 1991.

A. Kawamura and A. Pauly, Function spaces for second-order polynomial time, Conference on Computability in Europe, pp.245-254, 2014.
DOI : 10.1007/978-3-319-08019-2_25
URL : http://arxiv.org/pdf/1401.2861

G. Kreisel, Interpretation of analysis by means of constructive functionals of finite type, Constructivity in Mathematics, 1959.

M. Bruce, F. Kapron, and . Steinberg, Type-two polynomial-time and restricted lookahead, LICS, 2018.

A. Kawamura, F. Steinberg, and H. Thies, Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving, International Workshop on Logic, Language, Information, and Computation, pp.223-236, 2018.
DOI : 10.1007/978-3-662-57669-4_13
URL : https://hal.archives-ouvertes.fr/hal-02019142

A. Kawamura, F. Steinberg, and H. Thies, Second-order lineartime computability with applications in computable analysis. 15th Annual Conference on Theory and Applications of Models of Computation, 2019.
DOI : 10.1007/978-3-030-14812-6_21

C. Kreitz and K. Weihrauch, Theory of representations. Theoretical computer science, vol.38, pp.35-53, 1985.

D. Lacombe, Sur les possibilités d'extension de la notion de fonction récursive aux fonctions d'une ou plusieurs variables réelles, Le raisonnement en mathématiques et en sciences expérimentales, Colloques Internationaux du Centre National de la Recherche Scientifique, LXX, pp.67-75, 1958.

J. Longley and D. Normann, Higher-order computability, vol.100, 2015.
DOI : 10.1007/978-3-662-47992-6

R. S. Lubarsky and M. Rathjen, On the constructive dedekind reals, Logic and Analysis, vol.1, issue.2, pp.131-152, 2008.

, The Mathematical Components library

. Maximilianwuttke, Verified programming of Turing Machines in Coq, 2018.

K. Mehlhorn, Polynomial and abstract subrecursive classes, Journal of Computer and System Sciences, vol.12, issue.2, pp.147-178, 1976.

N. Th, S. Müller, N. Park, M. Preining, and . Ziegler, On formal verification in imperative multivalued programming over continuous data types, 2016.

E. Makarov and B. Spitters, The Picard algorithm for ordinary differential equations in Coq, ITP, vol.7998, pp.463-468, 2013.

N. Th and . Müller, The iRRAM: Exact arithmetic in C++, Computability and complexity in analysis. 4th international workshop, CCA, pp.222-252, 2000.

E. Neumann and F. Steinberg, Parametrised second-order complexity theory with applications to the study of interval computation, 2017.
URL : https://hal.archives-ouvertes.fr/hal-02019134

O. Russell and . Connor, Essential incompleteness of arithmetic verified by Coq, Theorem Proving in Higher Order Logics, pp.245-260, 2005.

O. Russell and . Connor, Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory, 2009.

A. Pauly, Multi-valued functions in computability theory, Conference on Computability in Europe, pp.571-580, 2012.

A. Pauly, On the topological aspects of the theory of represented spaces, Computability, vol.5, issue.2, pp.159-180, 2016.

M. Boykan-pour-el and J. Caldwell, On a simple definition of computable function of a real variable-with applications to functions of a complex variable, Mathematical Logic Quarterly, vol.21, issue.1, pp.1-19, 1975.

M. B. Pour-el and J. Richards, of Perspectives in Mathematical Logic, Computability in Analysis and Physics, vol.1, 1989.

A. Pauly and F. Steinberg, Comparing representations for function spaces in computable analysis. Theory of Computing Systems, vol.62, pp.557-582, 2018.

A. Pauly and M. Ziegler, Relative computability and uniform continuity of relations, J. Logic & Analysis, vol.5, 2013.

, Matthias Schröder. Extended admissibility. Theoretical computer science, vol.284, issue.2, pp.519-538, 2002.

M. Schröeder, Admissible Representations for Continuous Computations, 2002.

M. Schröder, Spaces allowing type-2 complexity theory revisited, Math. Log. Q, vol.50, pp.443-459, 2004.

A. L. Selman, A taxonomy of complexity classes of functions, Journal of Computer and System Sciences, vol.48, issue.2, pp.357-381, 1994.

. Robert-i-soare, Recursively enumerable sets and degrees, Bulletin of the American Mathematical Society, vol.84, issue.6, pp.1149-1181, 1978.

S. Selivanova and V. Selivanov, Computing solutions of symmetric hyperbolic systems of pde's. Electron. Notes Theor, Comput. Sci, vol.221, pp.243-255, 2008.

M. Schröder and F. Steinberg, Bounded time computation on metric spaces and Banach spaces, 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pp.1-12, 2017.

F. Steinberg, Computational Complexity Theory for Advanced Function Spaces in Analysis, 2017.

F. Steinberg, The CoqRep library, 2019.

F. Steinberg, The Incone library

F. Steinberg, The Metric library

F. Steinberg, The Mf library

F. Steinberg, The Rlzrs library

/. Floriansteinberg and . Rlzrs,

A. M. Turing, On computable numbers, with an application to the Entscheidungsproblem, Proceedings of the London Mathematical Society, vol.2, issue.1, pp.230-265, 1936.

A. Mathison and T. , On computable numbers, with an application to the Entscheidungsproblem. a correction, Proceedings of the London Mathematical Society, vol.2, issue.1, pp.544-546, 1938.

A. S. Troelstra and D. Van-dalen, of Studies in Logic and the Foundations of Mathematics, vol.II, 1988.

K. Weihrauch, Computability on computable metric spaces, Theoretical Computer Science, vol.113, issue.2, pp.191-210, 1993.

K. Weihrauch, Computable Analysis, 2000.