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. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Algorithms for minimization without derivatives, 1973. ,
, Lectures in Real Geometry, De Gruyter Expositions in Mathematics, vol.23, pp.1-67, 1996.
Introduction to Approximation Theory, 1966. ,
A certified infinite norm for the implementation of elementary functions, Proceedings of the Seventh International Conference on Quality Software, pp.153-160, 2007. ,
URL : https://hal.archives-ouvertes.fr/hal-02102507
Guaranteed proofs using interval arithmetic, Proceedings of the 17th IEEE Symposium on Computer Arithmetic, pp.188-195, 2005. ,
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, Lecture Notes in Computer Science, vol.2991, pp.64-90, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-02101997
Global optimization using interval analysis. Marcel Dekker, 1992. ,
Hol light: A tutorial introduction, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), vol.1166, pp.265-269, 1996. ,
Verifying nonlinear real formulas via sums of squares, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs, vol.4732, pp.102-118, 2007. ,
FI_LIB, eine schnelle und portable Funktionsbibliothek für reelle Argumente und reelle Intervalle im IEEE-double-Format, stitut für Wissenschaftliches Rechnen und Mathematische Modellbildung, 1998. ,
, Sponsored by the Microprocessor Standards Committee, IEEE Std, vol.754, p.2008, 2008.
Rigorous Global Search: Continuous Problems, 1996. ,
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 of the 15th IEEE Symposium on Computer Arithmetic, pp.111-118, 2001. ,
Floating-point arithmetic in the Coq system, RNC 8 Proceedings, 8th Conference on Real Numbers and Computers, pp.93-102, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-01780385
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. ,
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. ,
, Taylor forms-use and limits. Reliable Computing, vol.9, pp.43-79, 2003.
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, INRIA, 2001. ,
URL : https://hal.archives-ouvertes.fr/inria-00072518
Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematic, vol.162, issue.1, pp.33-50, 2004. ,
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