Proving the convergence of a sequence based on algebraic-geometric means to ?, 2013. ,
Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004. ,
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, Proceedings of the International Workshop on Types for proofs and programs (TYPES'06), pp.48-62, 2006. ,
DOI : 10.1007/978-3-540-74464-1_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.96.8457
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.200, issue.25???28, pp.423-456, 2013. ,
DOI : 10.1007/s10817-012-9255-4
URL : https://hal.archives-ouvertes.fr/hal-00649240
Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives, Proceedings of the 2nd International Conference on Certified Programs and Proofs (CPP), pp.289-304, 2012. ,
DOI : 10.1007/978-3-642-35308-6_22
URL : https://hal.archives-ouvertes.fr/hal-00712938
Formalization of real analysis: A survey of proof assistants and libraries. 2014. To be published in Mathematical Structures in Computer Science ,
URL : https://hal.archives-ouvertes.fr/hal-00806920
Reasoning about big enough numbers in Coq, Proceedings of the 4th Coq Workshop ,
C-CoRN, the Constructive Coq Repository at Nijmegen, Proceedings of the 3rd International Conference of Mathematical Knowledge Management (MKM), pp.88-103, 2004. ,
DOI : 10.1007/3-540-45620-1_12
A Constructive Formalization of the Fundamental Theorem of Calculus, Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'02), pp.108-126, 2003. ,
DOI : 10.1007/3-540-39185-1_7
Verified Real Number Calculations: A Library for Interval Arithmetic, IEEE Transactions on Computers, vol.58, issue.2, pp.226-237, 2009. ,
DOI : 10.1109/TC.2008.213
URL : https://hal.archives-ouvertes.fr/hal-00168402
Elements of mathematical analysis in PVS, Proceedings of the 9th International Conference Theorem Proving in Higher Order Logics (TPHOLs), pp.141-156, 1996. ,
DOI : 10.1007/BFb0105402
On the mechanization of real analysis in, Proceeding of the 13th International Conference of Theorem Proving in Higher Order Logics (TPHOLs), volume 1869 of Lecture Notes in Computer Science, pp.145-161, 2000. ,
Nonstandard analysis in ACL2, Journal of Automated Reasoning, vol.27, issue.4, pp.323-351, 2001. ,
DOI : 10.1023/A:1011908113514
Constructive Reals in Coq: Axioms and Categoricity, Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'00), volume 2277 of Lecture Notes in Computer Science, pp.79-95, 2002. ,
DOI : 10.1007/3-540-45842-5_6
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.97.6910
Constructing the real numbers in HOL. Formal Methods in System Design, pp.35-59, 1994. ,
Overview, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp.60-66, 2009. ,
DOI : 10.1007/978-1-4302-0821-1_1
URL : https://hal.archives-ouvertes.fr/in2p3-00803620
The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013. ,
DOI : 10.1007/s10817-012-9250-9
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP), pp.279-294, 2013. ,
DOI : 10.1007/978-3-642-39634-2_21
Computing with classical real numbers, Journal of Formalized Reasoning, vol.2, issue.1, pp.27-39, 2009. ,
Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, vol.9, issue.1, pp.1-27, 2013. ,
DOI : 10.2168/LMCS-9(1:1)2013
A new formalization of power series in Coq, 5th Coq Workshop, pp.1-2, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00880212
Différentiabilité et intégrabilité en Coq Applicationàtion`tionà la formule de d'Alembert, 23èmes Journées Francophones des Langages Applicatifs, pp.119-133, 2012. ,
Formalisation et automatisation de preuves en analyses réelle et numérique, 2001. ,
A Proof-Producing Decision Procedure for Real Arithmetic, Proceedings of the 20th International Conference on Automated Deduction, pp.295-314, 2005. ,
DOI : 10.1007/11532231_22
Proving Bounds on Real-Valued Functions with Computations, Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), pp.2-17, 2008. ,
DOI : 10.1007/978-3-540-71070-7_2
URL : https://hal.archives-ouvertes.fr/hal-00180138
Formalization of Bernstein Polynomials and Applications to Global Optimization, Journal of Automated Reasoning, vol.43, issue.1, pp.151-196, 2013. ,
DOI : 10.1007/s10817-012-9256-3
A Brief Overview of Mizar, Proceedings of the 22th International Conference on Theorem Proving in Higher Order Logics (TPHOLs), pp.67-72, 2009. ,
DOI : 10.1007/3-540-44755-5_26
PVS: A prototype verification system, Proceedings of the 11th International Conference on Automated Deduction (CADE), pp.748-752, 1992. ,
DOI : 10.1007/3-540-55602-8_217
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.28.2627
A monadic, functional implementation of real numbers, Mathematical Structures in Computer Science, vol.17, issue.1, pp.129-159, 2007. ,
A computer-verified monadic functional implementation of the integral, Theoretical Computer Science, vol.411, issue.37, pp.3386-3402, 2010. ,
Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics, Knowledge Exchange: Automated Provers and Proof Assistants, CEUR Workshop Proceedings, pp.67-76, 2008. ,
Subtypes for specifications: predicate subtyping in PVS, IEEE Transactions on Software Engineering, vol.24, issue.9, pp.709-720, 1998. ,
DOI : 10.1109/32.713327
Some features of the Mizar language, Proceedings of the ESPRIT Workshop, 1993. ,
Non negative real numbers. Part I, Journal of Formalized Mathematics, 1998. ,