Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002. ,
Rigorous uniform approximation of D-finite functions using Chebyshev expansions, Math. Comp, vol.86, issue.305, pp.1303-1341, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01022420
Iterative approximation of fixed points, Lecture Notes in Mathematics, vol.1912, 2007. ,
Verified integration of odes and flows using differential algebraic methods on high-order Taylor models, Reliable Computing, vol.4, issue.4, pp.361-369, 1998. ,
A Coq formal proof of the Lax-Milgram theorem, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01391578
Verifying Floating-point Algorithms with the Coq System, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01632617
Original French edition published by MASSON, 1971. ,
Validated and numerically efficient Chebyshev spectral methods for linear ordinary differential equations, ACM Transactions on Mathematical Software, 2018. ,
A New Lower Bound on the Hilbert Number for Quartic Systems, 2019. ,
Chebyshev interpolation polynomial-based tools for rigorous computing, Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, pp.147-154, 2010. ,
URL : https://hal.archives-ouvertes.fr/ensl-00472509
,
Formal and efficient primality proofs by use of computer algebra oracles, J. Symb. Comput, vol.32, issue.1, pp.55-70, 2001. ,
Estimating limit cycle bifurcations from centers, Differential equations with symbolic computation, pp.23-35, 2005. ,
, , 2014.
Chebyshev polynomials in numerical analysis, 1968. ,
Proving equalities in a commutative ring done right in coq, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs, vol.3603, pp.98-113, 2005. ,
A purely functional library for modular arithmetic and its application to certifying large prime numbers, Automated Reasoning, Third International Joint Conference, vol.4130, pp.423-437, 2006. ,
, , 2015.
A skeptic's approach to combining HOL and maple, J. Autom. Reasoning, vol.21, issue.3, pp.279-294, 1998. ,
Type classes and filters for mathematical analysis in isabelle/hol, Interactive Theorem Proving, pp.279-294, 2013. ,
Rigorous numerics for analytic solutions of differential equations: the radii polynomial approach, Math. Comp, vol.85, issue.299, pp.1427-1459, 2016. ,
A verified ODE solver and the Lorenz attractor, Journal of automated reasoning, pp.1-39, 2018. ,
Arb: efficient arbitrary-precision midpoint-radius interval arithmetic, IEEE Transactions on Computers, vol.66, issue.8, pp.1281-1292, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01394258
A quartic system with twenty-six limit cycles, Exp. Math, vol.20, issue.3, pp.323-328, 2011. ,
Rigorous Polynomial Approximations and Applications, 2011. ,
Self-validating numerics for function space problems: Computation with guarantees for differential and integral equations, vol.9, 1984. ,
C-XSC: A C++ class library for extended scientific computing, 2012. ,
Rigorous numerics for nonlinear differential equations using Chebyshev series, SIAM J. Numer. Anal, vol.52, issue.1, pp.1-22, 2014. ,
Formally verified approximations of definite integrals, Journal of Automated Reasoning, vol.62, issue.2, pp.281-300, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01289616
Proving tight bounds on univariate expressions with elementary functions in coq, Journal of Automated Reasoning, vol.57, issue.3, pp.187-217, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01086460
Proving bounds on real-valued functions with computations, International Joint Conference on Automated Reasoning, pp.2-17, 2008. ,
URL : https://hal.archives-ouvertes.fr/hal-00180138
Interval Analysis, 1966. ,
Motivations for an arbitrary precision interval arithmetic and the mpfi library, Reliable computing, vol.11, issue.4, pp.275-290, 2005. ,
URL : https://hal.archives-ouvertes.fr/inria-00100985
Intlab-interval laboratory, Developments in reliable computing, pp.77-104, 1999. ,
Approximation Theory and Approximation Practice. SIAM, 2013. ,
A rigorous ODE solver and Smale's 14th problem, Found. Comput. Math, vol.2, issue.1, pp.53-117, 2002. ,
Validated numerics: a short introduction to rigorous computations, 2011. ,
Chaotic braided solutions via rigorous numerics: Chaos in the Swift-Hohenberg equation, SIAM Journal on Applied Dynamical Systems, vol.7, issue.3, pp.988-1031, 2008. ,
A numerical verification method for solutions of boundary value problems with local uniqueness by Banach's fixed-point theorem, SIAM J. Numer. Anal, vol.35, issue.5, pp.2004-2013, 1998. ,