, TADIFF, a Flexible C++ Package for Automatic Differentiation Using Taylor Series, 1997.
, Interactive Theorem Proving and Program Development: Coq'Art: the Calculus of Inductive Constructions, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
, Algorithms for minimization without derivatives, N.J, 1973.
, Introduction to Approximation Theory, 1966.
, A Certified Infinite Norm for the Implementation of Elementary Functions, Seventh International Conference on Quality Software (QSIC 2007), pp.153-160, 2007.
DOI : 10.1109/QSIC.2007.4385491
URL : https://hal.archives-ouvertes.fr/ensl-00119810
, Guaranteed Proofs Using Interval Arithmetic, 17th IEEE Symposium on Computer Arithmetic (ARITH'05), pp.188-195, 2005.
DOI : 10.1109/ARITH.2005.25
URL : https://hal.archives-ouvertes.fr/hal-00164621
, Intégration numérique avec erreur bornée en précision arbitraire, 2006.
, Evaluating Derivatives -Principles and Techniques of Algorithmic Differentiation, 2000.
, Multiple Precision Interval Packages: Comparing Different Approaches, In Lecture Notes in Computer Science, vol.2991, pp.64-90, 2004.
DOI : 10.1007/978-3-540-24738-8_4
URL : https://hal.archives-ouvertes.fr/inria-00071744
, AN OVERVIEW OF GLOBAL OPTIMIZATION USING INTERVAL ANALYSIS, 1992.
DOI : 10.1016/B978-0-12-505630-4.50021-3
, HOL Light: A tutorial introduction, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), pp.265-269, 1996.
DOI : 10.1007/BFb0031814
, 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
, FI_LIB, eine schnelle und portable Funktionsbibliothek für reelle Argumente und reelle Intervalle im IEEE-double-Format, 1998.
, Rigorous Global Search: Continuous Problems, 1996.
DOI : 10.1007/978-1-4757-2495-0
, Globsol: History, composition, and advice on use, Global Optimization and Constraint Satisfaction, pp.17-31, 2003.
, Sichere und genaue Abschätzung des Approximationsfehlers bei rationalen Approximationen, 1996.
, Worst cases for correct rounding of the elementary functions in double precision, Proceedings 15th IEEE Symposium on Computer Arithmetic. ARITH-15 2001, pp.111-118, 2001.
DOI : 10.1109/ARITH.2001.930110
, Floating-point arithmetic in the Coq system, RNC 8 Proceedings, 8th Conference on Real Numbers and Computers, pp.93-102, 2008.
DOI : 10.1016/j.ic.2011.09.005
URL : https://hal.archives-ouvertes.fr/hal-00797913
, Méthodes d'optimisation globale basées sur l'analyse d'intervalle pour la résolution des problèmes avec contraintes, 1997.
, Methods and Applications of Interval Analysis, Society for Industrial Mathematics, 1979.
DOI : 10.1137/1.9781611970906
, ACETAF: A software package for computing validated bounds for Taylor coefficients of analytic functions, ACM Transactions on Mathematical Software, 2003.
, Interval Methods for Systems of Equations, 1990.
DOI : 10.1017/CBO9780511526473
, Taylor forms?use and limits, Reliable Computing, vol.9, issue.1, pp.43-79, 2003.
DOI : 10.1023/A:1023061927787
, PVS: A prototype verification system, 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992.
DOI : 10.1007/3-540-55602-8_217
, Efficient isolation of a polynomial real roots, 2001.
URL : https://hal.archives-ouvertes.fr/inria-00072518
, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics, vol.162, issue.1, pp.33-50, 2004.
DOI : 10.1016/j.cam.2003.08.015
, Formal Global Optimization with Taylor Models, IJCAR 2008 -Proceedings of the 4th International Joint Conference on Automated Reasoning, pp.408-422, 2008.
DOI : 10.1007/11814771_35
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.680.8497