. Mathematical-components-website, http://www.msr-inria.inria.fr/Projects/ math-components

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, ITP, pp.83-98, 2010.
DOI : 10.1007/978-3-642-14052-5_8

URL : https://hal.archives-ouvertes.fr/inria-00502496

A. Asperti, C. Sacerdoti-coen, E. Tassi, and S. Zacchiroli, User Interaction with the Matita Proof Assistant, Journal of Automated Reasoning, vol.11, issue.3, pp.109-139, 2007.
DOI : 10.1007/s10817-007-9070-5

H. Bender and G. Glauberman, Local analysis for the Odd Order Theorem . Number 188 in London Mathematical Society Lecture Note Series, 1994.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development , Coq'Art: the Calculus of Inductive Constructions, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

Y. Bertot, G. Kahn, and L. Théry, Proof by pointing, TACS, LNCS, pp.141-160, 1994.
DOI : 10.1007/3-540-57887-0_94

URL : https://hal.archives-ouvertes.fr/inria-00073402

T. Braibant and D. Pous, An Efficient Coq Tactic for Deciding Kleene Algebras, ITP, pp.163-178, 2010.
DOI : 10.1007/978-3-642-14052-5_13

T. Braibant and D. Pous, Tactics for Reasoning Modulo AC in Coq, CPP, pp.167-182, 2011.
DOI : 10.1007/978-3-540-71067-7_23

URL : https://hal.archives-ouvertes.fr/hal-00484871

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11

URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection extension for the Coq system, p.258384
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, Formal proof ? the four color theorem. Notices of the, pp.1382-1394, 2008.

B. Grégoire and A. Mahboubi, Proving Equalities in a Commutative Ring Done Right in Coq, TPHOLs, pp.98-113, 2005.
DOI : 10.1007/11541868_7

B. Huppert and N. Blackburn, Finite groups II, Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, 1982.
DOI : 10.1007/978-3-642-67994-0

C. Lawrence and . Paulson, The foundation of a generic theorem prover, Journal of Automated Reasoning, vol.5, pp.363-397, 1989.

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

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

B. Spitters and E. Van-der-weegen, Type classes for mathematics in type theory, Mathematical Structures in Computer Science, vol.2, issue.04, pp.1-31, 2011.
DOI : 10.1007/3-540-48256-3_10

L. Théry and G. Hanrot, Primality Proving with Elliptic Curves, TPHOLs, pp.319-333, 2007.
DOI : 10.1007/978-3-540-74591-4_24

M. Wenzel, Isar ??? A Generic Interpretative Approach to Readable Formal Proof Documents, TPHOLs, pp.167-184, 1999.
DOI : 10.1007/3-540-48256-3_12