Formalizing functional analysis structures in dependent type theory (accompanying material ,
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
, analysis Team: Mathematical components compliant analysis library, 2017.
Hints in unification, 22nd International Conference on Theorem Proving in Higher Order Logics, vol.5674, pp.84-98, 2009. ,
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. ,
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
, Mathematical Components Team: Mathematical Components library, 2007.
, L??N THEOREM PROVER, 2020.
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, The Coq Workshop, 2019. ,
, 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 mathlib Community: The Lean mathematical library, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp.367-381, 2019.