P. Jackson, Enhancing the Nuprl proof-development system and applying it to computational abstract algebra, 1995.

G. Betarte and A. Tasistro, Formalisation of systems of algebras using dependent record types and subtyping: An example, Proc. 7th Nordic workshop on Programming Theory, 1995.

L. Pottier, User contributions in Coq, Algebra, 1999.

H. Geuvers, R. Pollack, F. Wiedijk, and J. Zwanenburg, A Constructive Algebraic Hierarchy in Coq, Journal of Symbolic Computation, vol.34, issue.4, pp.271-286, 2002.
DOI : 10.1006/jsco.2002.0552

F. Haftmann and M. Wenzel, Local Theory Specifications in Isabelle/Isar, Types for Proofs and Programs, TYPES 2008 International Workshop, Selected Papers, 2009.
DOI : 10.1007/978-3-540-74591-4_26

P. Rudnicki, C. Schwarzweller, and A. Trybulec, Commutative Algebra in the Mizar System, Journal of Symbolic Computation, vol.32, issue.1-2, pp.143-169, 2001.
DOI : 10.1006/jsco.2001.0456

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, LNCS, vol.4732, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pasca, Canonical Big Operators, LNCS, vol.33, issue.1, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

C. Paulin-mohring, Définitions Inductives en Théorie des Types d'Ordre Supérieur. HabilitationàHabilitation`Habilitationà diriger les recherches, 1996.

M. Sozeau and N. Oury, First-Class Type Classes, Lecture Notes in Computer Science, vol.5170, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

R. Pollack, Dependently Typed Records in Type Theory, Formal Aspects of Computing, vol.13, issue.3-5, pp.386-402, 2002.
DOI : 10.1007/s001650200018

N. G. Bruijn, Telescopic mappings in typed lambda calculus, Information and Computation, vol.91, issue.2, pp.189-204, 1991.
DOI : 10.1016/0890-5401(91)90066-B

L. C. Paulson, Defining functions on equivalence classes, ACM Transactions on Computational Logic, vol.7, issue.4, pp.658-675, 2006.
DOI : 10.1145/1183278.1183280

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.57-68, 2007.
DOI : 10.1145/1292597.1292608
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.207.4309

G. Olteanu, Computing the Wedderburn decomposition of group algebras by the Brauer-Witt theorem, Mathematics of Computation, vol.76, issue.258, pp.1073-1087, 2007.
DOI : 10.1090/S0025-5718-07-01957-6

J. J. Rotman, An Introduction to the Theory of Groups, 1994.
DOI : 10.1007/978-1-4612-4176-8

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein, Introduction to Algorithms, 2003.

C. Sacerdoti-coen and E. Tassi, Working with Mathematical Structures in Type Theory, Proceedings of TYPES 2007: Conference of the Types Project, pp.157-172, 2008.
DOI : 10.1007/978-3-540-68103-8_11

C. Sacerdoti-coen and E. Tassi, A constructive and formal proof of Lebesgue Dominated Convergence Theorem in the interactive theorem prover Matita, Journal of Formalized Reasoning, vol.1, pp.51-89, 2008.