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

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

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, G. Gilbert, P. G. Haselwarter, M. Pretnar, and C. A. Stone, Design and implementation of the andromeda proof assistant, 2018.

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.

C. Cohen, 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

C. Cohen and A. Mahboubi, 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

C. Cohen, K. Sakaguchi, and E. Tassi, Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi (2020), accepted in the proceedings of FSCD 2020

R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer et al., Implementing Mathematics with the NuPRL Proof Development System, 1986.

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

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

L. M. De-moura, S. Kong, J. Avigad, F. Van-doorn, and J. Von-raumer, The lean theorem prover (system description), Automated Deduction -CADE-25 -25th International Conference on Automated Deduction, vol.9195, pp.378-388, 2015.

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, 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020.

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 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.