R. Affeldt, C. Cohen, M. Kerjean, A. Mahboubi, D. Rouhling et al., Formalizing functional analysis structures in dependent type theory (accompanying material

R. Affeldt, C. Cohen, and D. Rouhling, 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.

A. Asperti, W. Ricciotti, C. Sacerdoti-coen, and E. Tassi, Hints in unification, 22nd International Conference on Theorem Proving in Higher Order Logics, vol.5674, pp.84-98, 2009.

A. Bauer, J. Gross, P. L. Lumsdaine, M. Shulman, M. Sozeau et al., 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

Y. Bertot, G. Gonthier, S. O. Biha, and I. Pasca, 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

S. Boldo, C. Lelay, and G. Melquiond, 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

N. Bourbaki, The architecture of mathematics, The American Mathematical Monthly, vol.57, issue.4, pp.221-232, 1950.

N. Bourbaki, Théorie des ensembles, Éléments de mathématique, 1970.

N. G. De-bruijn, Telescopic mappings in typed lambda calculus, Information and Computation, vol.91, issue.2, pp.189-204, 1991.

K. Buzzard, J. Commelin, and P. Massot, Formalising perfectoid spaces, 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp.299-312, 2020.

T. Coquand and C. Paulin, Inductively defined types, International Conference on Computer Logic (COLOG-88), vol.417, pp.50-66, 1988.

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging mathematical structures, Theorem Proving in Higher-Order Logics, vol.5674, pp.327-342, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier, A. Asperti, J. Avigad, Y. Bertot, C. Cohen et al., 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

J. Harrison, The HOL Light System REFERENCE, 2017.

A. Mahboubi and E. Tassi, 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.

M. Reasearch, L??N THEOREM PROVER, 2020.

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle HOL: A Proof Assistant for Higher-Order Logic, 2019.

A. Saïbi, Applicationà la Théorie des Catégories. (Formalization of Mathematics in Type Theory. Generic tools of Modelisation and Demonstration. Application to Category Theory), 1999.

K. Sakaguchi, Validating mathematical structures, The Coq Workshop, 2019.

D. Selsam, S. Ullrich, and L. De-moura, Tabled typeclass resolution, 2020.

M. Sozeau and N. Oury, 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

B. Spitters and E. Van-der-weegen, 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.