A. Adje, S. Gaubert, and E. Goubault, Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, Logical methods in computer science, vol.8, issue.1, pp.1-32, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00782742

M. Akian, S. Gaubert, and V. Kolokoltsov, Set coverings and invertibility of functional Galois connections, Idempotent Mathematics and Mathematical Physics Contemporary Mathematics, vol.377, pp.19-51, 2005.
DOI : 10.1090/conm/377/06983

URL : https://hal.archives-ouvertes.fr/inria-00000966

]. M. Agl08a, S. Akian, A. Gaubert, and . Lakhoua, The max-plus finite element method for solving deterministic optimal control problems: basic properties and convergence analysis, SIAM J. Control Optim, vol.47, issue.2, pp.817-848, 2008.

M. Akian, S. Gaubert, and A. Lakhoua, The Max-Plus Finite Element Method for Solving Deterministic Optimal Control Problems: Basic Properties and Convergence Analysis, SIAM Journal on Control and Optimization, vol.47, issue.2, pp.817-848, 2008.
DOI : 10.1137/060655286

URL : https://hal.archives-ouvertes.fr/inria-00071395

S. Agmw13a-]-xavier-allamigeon, V. Gaubert, B. Magron, and . Werner, Certification of bounds of non-linear functions : the templates method, 2013, To appear in the Proceedings of Conferences on Intelligent Computer Mathematics, CICM 2013 Calculemus

S. Agmw13b-]-xavier-allamigeon, V. Gaubert, B. Magron, and . Werner, Certification of inequalities involving transcendental functions: combining sdp and max-plus approximation, 2013, To appear in the Proceedings of the European Control Conference, p.13

B. Armand, A. Grégoire, L. Spiwack, and . Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8

URL : https://hal.archives-ouvertes.fr/inria-00502496

K. Appel and W. Haken, Every planar map is 4-colorable, Illinois Journal of Mathematics, vol.21, pp.429-567, 1977.
DOI : 10.1090/s0002-9904-1976-14122-5

URL : http://projecteuclid.org/download/pdf_1/euclid.bams/1183538218

M. M. Ali, C. Khompatraporn, and Z. B. Zabinsky, A Numerical Evaluation of Several Stochastic Algorithms on Selected Continuous Global Optimization Test Problems, Journal of Global Optimization, vol.3, issue.3, pp.635-672, 2005.
DOI : 10.1007/s10898-004-9972-2

B. Akbarpour and L. C. Paulson, MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions, Journal of Automated Reasoning, vol.7, issue.4, pp.175-205, 2010.
DOI : 10.1007/s10817-009-9149-2

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, 2004.
DOI : 10.1007/978-3-662-07964-5

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

S. Burgdorf, K. Cafuta, I. Klep, and J. Povh, The tracial moment problem and trace-optimization of polynomials, Mathematical Programming, pp.557-578, 2013.
DOI : 10.1007/s10107-011-0505-8

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

F. Besson, Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Proceedings of the 2006 international conference on Types for proofs and programs, TYPES'06, pp.48-62, 2007.
DOI : 10.1007/978-3-540-74464-1_4

N. Brisebarre, M. Joldes, and M. , Chebyshev interpolation polynomial-based tools for rigorous computing, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC '10, pp.147-154, 2010.
DOI : 10.1145/1837934.1837966

URL : https://hal.archives-ouvertes.fr/ensl-00472509

J. [. Boyer and . Moore, Metafunctions: Proving them correct and using them efficiently as new proof procedures, The Correctness Problem in Computer Science, pp.103-84, 1981.

M. Berz and K. Makino, Rigorous global search using taylor models, Proceedings of the 2009 conference on Symbolic numeric computation, SNC '09, pp.11-20, 2009.
DOI : 10.1145/1577190.1577198

B. Borchers, CSDP, A C library for semidefinite programming, Optimization Methods and Software, vol.6, issue.1-4, 1997.
DOI : 10.1145/292395.292412

G. Barthe, M. Ruys, and H. Barendregt, A two-level approach towards lean proof-checking, 1996.
DOI : 10.1007/3-540-61780-9_59

A. Ben-tal and A. Nemirovski, Lectures on modern convex optimization: analysis, algorithms, and engineering applications, Society for Industrial and Applied Mathematics, 2001.
DOI : 10.1137/1.9780898718829

F. [. Cuyt, C. Backeljauw, and . Bonan-hamada, Handbook of Continued Fractions for Special Functions. SpringerLink: Springer e-Books, 2008.

G. Calafiore and F. Dabbene, Reduced Vertex Set Result for Interval Semidefinite Optimization Problems, Journal of Optimization Theory and Applications, vol.8, issue.1, pp.17-33, 1007.
DOI : 10.1007/s10957-008-9423-1

J. Sylvain-conchon, J. Filliâtre, and . Signoles, Designing a Generic Graph Library using ML Functors, The Eighth Symposium on Trends in Functional Programming, pp.1-13, 2007.

[. Cartis, N. I. Gould, and P. L. Toint, Adaptive cubic regularisation methods for unconstrained optimization. Part I: motivation, convergence and numerical results, Mathematical Programming, vol.22, issue.3, pp.245-295, 2011.
DOI : 10.1007/s10107-009-0286-5

E. W. Cheney, Introduction to Approximation Theory, 1982.

S. Chevillard, Évaluation efficace de fonctions numériques -Outils et exemples. These, 2009.

J. Cimpric, A method for computing lowest eigenvalues of symmetric polynomial differential operators by semidefinite programming. ArXiv e-prints, 2009.

S. Chevillard, M. Joldes, and C. Lauter, Certified and Fast Computation of Supremum Norms of Approximation Errors, 2009 19th IEEE Symposium on Computer Arithmetic, pp.169-176, 2009.
DOI : 10.1109/ARITH.2009.18

URL : https://hal.archives-ouvertes.fr/ensl-00334545

M. [. Chevillard, C. Joldes, and . Lauter, Sollya: An Environment for the Development of Numerical Codes, Mathematical Software -ICMS 2010, pp.28-31, 2010.
DOI : 10.1007/978-3-642-15582-6_5

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

K. Cafuta, I. Klep, and J. Povh, Ncsostools: a computer algebra system for symbolic and numerical computation with noncommutative polynomials. Optimization Methods and Software, pp.363-380, 2011.

A. Connes, Classification of Injective Factors Cases II 1 , II ??? , III ?? , ?? ??? 1, The Annals of Mathematics, vol.104, issue.1, pp.73-115, 1976.
DOI : 10.2307/1971057

M. Etienne-de-klerk and . Laurent, Error Bounds for Some Semidefinite Programming Approaches to Polynomial Minimization on the Hypercube, SIAM Journal on Optimization, vol.20, issue.6, pp.3104-3120, 2010.
DOI : 10.1137/100790835

W. [. Fleming and . Mceneaney, A Max-Plus-Based Algorithm for a Hamilton--Jacobi--Bellman Equation of Nonlinear Filtering, SIAM Journal on Control and Optimization, vol.38, issue.3, pp.683-710, 2000.
DOI : 10.1137/S0363012998332433

S. Gao, J. Avigad, and E. M. Clarke, Delta-complete decision procedures for satisfiability over the reals, 1204.

[. Gvozdenovic, M. Laurent, and F. Vallentin, Block-diagonal semidefinite programming hierarchies for 0/1 programming, Operations Research Letters, vol.37, issue.1, pp.27-31, 2009.
DOI : 10.1016/j.orl.2008.10.003

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, Lecture Notes in Computer Science, vol.3603, pp.98-113, 2005.
DOI : 10.1007/11541868_7

S. Gaubert, W. M. Mceneaney, and Z. Qu, Curse of dimensionality reduction in max-plus based approximation methods: Theoretical estimates and improved pruning algorithms, IEEE Conference on Decision and Control and European Control Conference, pp.1054-1061, 2011.
DOI : 10.1109/CDC.2011.6161386

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

G. Gonthier, Computer mathematics. chapter The Four Colour Theorem: Engineering of a Formal Proof, pp.333-333, 2008.

B. Grégoire and L. Thery, A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers, Proceedings of IJCAR'06, pp.423-437, 2006.
DOI : 10.1007/11814771_36

[. Grégoire, L. Théry, and B. Werner, A Computational Approach to Pocklington Certificates in Type Theory, Functional and Logic Programming, pp.97-113, 2006.
DOI : 10.1007/11737414_8

C. Thomas and . Hales, A proof of the kepler conjecture, Math. Intelligencer, vol.16, pp.47-58, 1994.

C. Thomas and . Hales, Some algorithms arising in the proof of the kepler conjecture, Discrete and Computational Geometry, pp.489-507, 2003.

C. Thomas and . Hales, A proof of the Kepler conjecture, Ann. of Math, vol.162, issue.23, pp.1065-1185, 2005.

C. Thomas and . Hales, Introduction to the flyspeck project, Mathematics , Algorithms and Proofs, number 05021 in Dagstuhl Seminar Proceedings Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, 2006.

C. Thomas and . Hales, The flyspeck project, 2013.

E. R. Hansen, Sharpening Interval Computations, Reliable Computing, vol.22, issue.1, pp.21-34, 2006.
DOI : 10.1007/s11155-006-2967-6

J. Harrison, Verifying Nonlinear Real Formulas Via Sums of Squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, pp.102-118, 2007.
DOI : 10.1007/978-3-540-74591-4_9

H. A. Helfgott, Major arcs for Goldbach's theorem. ArXiv e-prints, 2013.

E. R. Hansen and R. I. Greenberg, An interval Newton method, Applied Mathematics and Computation, vol.12, issue.2-3, pp.89-98, 1983.
DOI : 10.1016/0096-3003(83)90001-2

D. Henrion, J. Lasserre, and C. Savorgnan, POCP: a package for polynomial optimal control problems, 2008.
URL : https://hal.archives-ouvertes.fr/hal-00325180

H. A. Helfgott and D. J. Platt, Numerical Verification of the Ternary Goldbach Conjecture up to 8.875e30. ArXiv e-prints, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00827998

[. Kim, M. Kojima, and H. Waki, Generalized Lagrangian Duals and Sums of Squares Relaxations of Sparse Polynomial Optimization Problems, SIAM Journal on Optimization, vol.15, issue.3, 2004.
DOI : 10.1137/030601260

[. Kojima, S. Kim, and H. Waki, Sparsity in sums of squares of polynomials, Mathematical Programming, vol.23, issue.1, 2004.
DOI : 10.1007/s10107-004-0554-3

E. L. Kaltofen, B. Li, Z. Yang, and L. Zhi, Exact certification in global polynomial optimization via sums-of-squares of rational functions with rational coefficients, memory of Wenda Wu, pp.1-15, 1929.
DOI : 10.1016/j.jsc.2011.08.002

A. Karatsuba and Y. Ofman, Multiplication of Multidigit Numbers on Automata, Soviet Physics-Doklady, vol.7, pp.595-596, 1963.

I. Klep and M. Schweighofer, Sums of Hermitian Squares and the BMV Conjecture, Journal of Statistical Physics, vol.10, issue.1???4, pp.739-760, 2008.
DOI : 10.1007/s10955-008-9632-x

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

J. B. Lasserre, Convergent SDP???Relaxations in Polynomial Optimization with Sparsity, SIAM Journal on Optimization, vol.17, issue.3, pp.822-843
DOI : 10.1137/05064504X

J. B. Lasserre, Global Optimization with Polynomials and the Problem of Moments, SIAM Journal on Optimization, vol.11, issue.3, pp.796-817, 2001.
DOI : 10.1137/S1052623400366802

M. Laurent, Matrix completion problems, Encyclopedia of Optimization, pp.1967-1975, 2009.
DOI : 10.1007/0-306-48332-7_271

P. D. Lax, Differential equations, difference equations and matrix theory, Communications on Pure and Applied Mathematics, vol.7, issue.2, pp.175-194, 1958.
DOI : 10.1002/cpa.3160110203

J. Lasserre, D. Henrion, C. Prieur, and E. Trélat, Nonlinear Optimal Control via Occupation Measures and LMI-Relaxations, SIAM Journal on Control and Optimization, vol.47, issue.4, pp.1643-1666, 2008.
DOI : 10.1137/070685051

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

B. Jean, M. Lasserre, and . Putinar, Positivity and optimization for semi-algebraic functions, SIAM Journal on Optimization, vol.20, issue.6, pp.3364-3383, 2010.

E. H. Lieb and R. Seiringer, Equivalent Forms of the Bessis???Moussa???Villani Conjecture, Journal of Statistical Physics, vol.115, issue.1/2, pp.185-190, 2004.
DOI : 10.1023/B:JOSS.0000019811.15510.27

. Jeanb, T. Lasserre, and . Thanh, Convex underestimators of polynomials, Journal of Global Optimization, vol.56, issue.1, pp.1-25, 2013.

G. D. Maso, An Introduction to Gamma-Convergence, 1993.

D. Monniaux and P. Corbineau, On the Generation of Positivstellensatz Witnesses in Degenerate Cases, Interactive Theorem Proving (ITP), pp.249-264, 2011.
DOI : 10.1137/1038003

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

W. M. Mceneaney, Max-plus methods for nonlinear control and estimation. Systems & Control: Foundations & Applications, Birkhäuser Boston Inc, 2006.

W. M. Mceneaney, A Curse-of-Dimensionality-Free Numerical Method for Solution of Certain HJB PDEs, SIAM Journal on Control and Optimization, vol.46, issue.4, pp.1239-1276, 2007.
DOI : 10.1137/040610830

W. M. Mceneaney, A. Deshpande, and S. Gaubert, Curse-of-complexity attenuation in the curse-of-dimensionality-free method for HJB PDEs, 2008 American Control Conference
DOI : 10.1109/ACC.2008.4587234

G. Melquiond, Floating-point arithmetic in the coq system Information and Computation, <ce:title>Special Issue: 8th Conference on Real Numbers and Computers<, pp.14-23, 2012.

F. Messine, Extensions of affine arithmetic: Application to unconstrained global optimization, 1999.

J. C. Mason and D. D. Handscomb, The Chebyshev Polynomials, 2003.
DOI : 10.1201/9781420036114

M. Tiago and . Montanher, Intsolver: An interval based toolbox for global optimization, 2009.

J. Nagata, Modern general topology. Bibliotheca mathematica, 1974.

Y. Nesterov and A. Nemirovski, Interior Point Polynomial Methods in Convex Programming: Theory and Applications, Society for Industrial and Applied Mathematics, 1994.

J. Nie and M. Schweighofer, On the complexity of Putinar's Positivstellensatz, Journal of Complexity, vol.23, issue.1, pp.135-150, 2007.
DOI : 10.1016/j.jco.2006.07.002

T. Netzer and A. Thom, Hyperbolic Polynomials and Generalized Clifford Algebras. ArXiv e-prints, 2012.
DOI : 10.1007/s00454-014-9598-1

URL : http://arxiv.org/abs/1207.3159

H. Peyrl and P. A. Parrilo, Computing sum of squares decompositions with rational coefficients, Theoretical Computer Science, vol.409, issue.2, pp.269-281, 2008.
DOI : 10.1016/j.tcs.2008.09.025

A. Pablo, B. Parrilo, and . Sturmfels, Minimizing polynomial functions, DIMACS Ser. Discrete Math. Theoret. Comput. Sci. Amer. Math. Soc, vol.60, pp.83-99, 2003.

R. T. Rockafellar, Convex Analysis. Princeton mathematical series, 1970.

[. Riener, T. Theobald, L. J. Andrén, and J. B. Lasserre, Exploiting Symmetries in SDP-Relaxations for Polynomial Optimization, Mathematics of Operations Research, vol.38, issue.1, 2011.
DOI : 10.1287/moor.1120.0558

M. Schweighofer, On the complexity of Schm??dgen's Positivstellensatz, Journal of Complexity, vol.20, issue.4, pp.529-543, 2004.
DOI : 10.1016/j.jco.2004.01.005

M. Schweighofer, Optimization of Polynomials on Compact Semialgebraic Sets, SIAM Journal on Optimization, vol.15, issue.3, pp.805-825, 2005.
DOI : 10.1137/S1052623403431779

[. Sridharan, M. Gu, M. R. James, and W. M. Mceneaney, Reduced-complexity numerical method for optimal gate synthesis, Physical Review A, vol.82, issue.4, p.42319, 2010.
DOI : 10.1103/PhysRevA.82.042319

A. Solovyev and T. C. Hales, Formal verification of nonlinear inequalities with taylor interval approximations. CoRR, abs, 1301.

[. Spiwack, Ajouter des entiers machine à coq, 2006.

[. Sankaranarayanan, H. B. Sipma, and Z. Manna, Scalable Analysis of Linear Systems Using Mathematical Programming, Proc. of Verification, Model Checking and Abstract Interpretation (VMCAI), pp.21-47, 2005.
DOI : 10.1007/978-3-540-30579-8_2

H. R. Stahl, Proof of the BMV Conjecture. ArXiv e-prints, 2011.

F. Jos and . Sturm, Using sedumi 1.02, a matlab toolbox for optimization over symmetric cones, 1998.

L. Vandenberghe and S. Boyd, Semidefinite Programming, SIAM Review, vol.38, issue.1, pp.49-95, 1994.
DOI : 10.1137/1038003

S. Waki, M. Kim, M. Kojima, H. Muramatsu, and . Sugimoto, Algorithm 883, ACM Transactions on Mathematical Software, vol.35, issue.2, 2008.
DOI : 10.1145/1377612.1377619

[. Waki, S. Kim, M. Kojima, and M. Muramatsu, Sums of Squares and Semidefinite Program Relaxations for Polynomial Optimization Problems with Structured Sparsity, SIAM Journal on Optimization, vol.17, issue.1, pp.218-242, 2006.
DOI : 10.1137/050623802

K. Yamashita, K. Fujisawa, M. Nakata, M. Nakata, K. Fukuda et al., A highperformance software package for semidefinite programs : Sdpa7, Dept. of Information Sciences, 2010.

R. Zumkeller, Rigorous Global Optimization, 2008.