Classical analysis with Coq, Analysis library compatible with Mathematical Components, 2018. ,
Formalizing O notation in Isabelle/HOL, Proceedings of the Second International Joint Conference on Automated Reasoning, vol.3097, p.357371, 2004. ,
Cours de mathématiques, Analyse. Dunod, vol.2, 1988. ,
, Proceedings of the 8th International Conference on Interactive Theorem Proving, vol.10499, 2017.
Die Analytische Zahlentheorie. B.G. Teubner, 1894 ,
Wave Equation Numerical Resolution: A Comprehensive Mechanized Proof of a C Program, Journal of Automated Reasoning, vol.50, issue.4, p.423456, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00649240
Formalization of the Lindemann-Weierstrass theorem, Ayala-Rincón and Muñoz, p.6580 ,
URL : https://hal.archives-ouvertes.fr/hal-01647563
,
Coquelicot: A User-Friendly Library of Real Analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, p.4162, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-00860648
The Coquelicot library, 2018. ,
, Proceedings of the 4th International Conference on Interactive Theorem Proving, ITP 2013, 2013.
Construction of real algebraic numbers in Coq, Proceedings of the Third International Conference on Interactive Theorem Proving, ITP 2012, vol.7406, p.6782, 1315. ,
URL : https://hal.archives-ouvertes.fr/hal-00671809
Formalized algebraic numbers: construction and rstorder theory, 2012. ,
, The Coq Development Team. The Coq proof assistant reference manual, 2018.
A Formal Proof in Coq of LaSalle's Invariance Principle, vol.148, p.163 ,
Axiom of choice and complementation, Proceedings of the American Mathematical Society, vol.51, p.176178, 1975. ,
Proving divide and conquer complexities in Is ,
, Journal of Automated Reasoning, vol.58, issue.4, p.483508, 2017.
The Mathematical Components repository ,
,
A Machine-Checked Proof of the Odd Order Theorem, vol.13, p.163179 ,
URL : https://hal.archives-ouvertes.fr/hal-00816699
A stful of dollars: Formalizing asymptotic complexity claims via deductive program verication, Proceedings of the 27th European Symposium on Programming on Programming Languages and Systems, ESOP 2018, held as part of the European Joint Conferences on Theory and Practice of Software, vol.2018, p.533560, 1420. ,
Packaging mathematical structures, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, vol.5674, p.327342, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00368403
An introduction to small scale reection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, p.95152, 2010. ,
A Small Scale Reection Extension for the Coq system, 2016. ,
Point-free, set-free concrete linear algebra, Proceeding of the 2nd International Conference on Interactive Theorem Proving, vol.6898, pp.103-118, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00805966
Procrastination, a proof engineering technique, Coq Workshop, 2018. ,
Type Classes and Filters for Mathematical Analysis in Isabelle/HOL, vol.13, p.279294 ,
Teach Calculus with Big O. Notices of the AMS, vol.45, p.687688, 1998. ,
,
, Handbuch der Lehre von der Verteilung der Primzahlen, 1909.
, The Lean mathematical components library developers. Lean mathematical components library
Canonical Structures for the Working Coq User, vol.13, p.1934 ,
URL : https://hal.archives-ouvertes.fr/hal-00816703
,
, Mathematical Components. Available
A Formal Proof in Coq of a Control Function for the Inverted Pendulum, Proceedings of the 7th ACM SIGPLAN International Conference on Certied Programs and Proofs, vol.2018, p.2841, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01639819
, coq-topology: Topology library for Coq, 2011.
coq-zorns-lemma: Naive set theory library for Coq, 2011. ,
First-class type classes, Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs, vol.5170, p.278293, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00628864
, The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics, 2013.