Formalizing functional analysis structures in dependent type theory (accompanying material, 2020. ,
Formalization Techniques for Asymptotic Reasoning in Classical Analysis, Journal of Formalized Reasoning, vol.11, pp.43-76, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01719918
Hints in unification, 22nd International Conference on Theorem Proving in Higher Order Logics, vol.5674, pp.84-98, 2009. ,
Design and implementation of the andromeda proof assistant, 2018. ,
The HoTT library: a formalization of homotopy type theory in Coq, 6th ACM SIG-PLAN Conference on Certified Programs and Proofs (CPP 2017), pp.164-172, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01421212
Canonical big operators, 21st International Conference on Theorem Proving in Higher Order Logics, vol.5170, pp.86-101, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00331193
Coquelicot: A user-friendly library of real analysis for Coq, Mathematics in Computer Science, vol.9, issue.1, pp.41-62, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-00860648
The architecture of mathematics, The American Mathematical Monthly, vol.57, issue.4, pp.221-232, 1950. ,
Théorie des ensembles, Éléments de mathématique, 1970. ,
Telescopic mappings in typed lambda calculus, Information and Computation, vol.91, issue.2, pp.189-204, 1991. ,
Formalising perfectoid spaces, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp.299-312, 2020. ,
Formalized algebraic numbers: construction and first-order theory. (Formalisation des nombres algébriques : construction et théorie du premier ordre), 2012. ,
URL : https://hal.archives-ouvertes.fr/pastel-00780446
Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination, Logical Methods in Computer Science, vol.8, issue.1, 2012. ,
URL : https://hal.archives-ouvertes.fr/inria-00593738
Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (2020), accepted in the proceedings of FSCD 2020 ,
Implementing Mathematics with the NuPRL Proof Development System, 1986. ,
Inductively defined types, International Conference on Computer Logic (COLOG-88), vol.417, pp.50-66, 1988. ,
Packaging mathematical structures, Theorem Proving in Higher-Order Logics, vol.5674, pp.327-342, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00368403
A machine-checked proof of the odd order theorem, 4th International Conference on Interactive Theorem Proving (ITP 2013), vol.7998, pp.163-179, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00816699
, The HOL Light System REFERENCE, 2017.
Canonical structures for the working Coq user, 4th International Conference on Interactive Theorem Proving (ITP 2013), vol.7998, pp.19-34, 2013. ,
URL : https://hal.archives-ouvertes.fr/hal-00816703
, L??N THEOREM PROVER, 2020.
The lean theorem prover (system description), Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.378-388, 2015. ,
Isabelle HOL: A Proof Assistant for Higher-Order Logic, 2019. ,
Applicationà la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory), 1999. ,
Validating mathematical structures, 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020. ,
, Tabled typeclass resolution, 2020.
First-Class Type Classes, 21st International Conference on Theorem Proving in Higher Order Logics, vol.5170, pp.278-293, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00628864
Type classes for mathematics in type theory, Mathematical Structures in Computer Science, vol.21, issue.4, pp.795-825, 2011. ,
, The Agda Team: The Agda User Manual, 2020.
, The Coq Development Team: The Coq Proof Assistant Reference Manual, Inria, 2019.
, The Mathematical Components Analysis Team: The Mathematical Components Analysis library, 2017.
, The Mathematical Components Team: The Mathematical Components library, 2007.
, The mathlib Community: The Lean mathematical library, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp.367-381, 2020.