M. Barakat and M. Lange-hegermann, AN AXIOMATIC SETUP FOR ALGORITHMIC HOMOLOGICAL ALGEBRA AND AN ALTERNATIVE APPROACH TO LOCALIZATION, Journal of Algebra and Its Applications, vol.10, issue.02, pp.269-293, 2011.
DOI : 10.1142/S0219498811004562

M. Barakat and D. Robertz, homalg ??? A META-PACKAGE FOR HOMOLOGICAL ALGEBRA, Journal of Algebra and Its Applications, vol.07, issue.03, pp.299-317, 2008.
DOI : 10.1142/S0219498808002813

Y. Bertot, G. Gonthier, S. Biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

G. Cano and M. Dénès, Matrices à blocs et en forme canonique, JFLA -Journées francophones des langages applicatifs
URL : https://hal.archives-ouvertes.fr/hal-00779376

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, Certified Programs and Proofs, pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

C. Cohen and A. Mahboubi, A Formal Quantifier Elimination for Algebraically Closed Fields, Proceedings of the 10th ASIC and 9th MKM international conference , and 17th Calculemus conference on Intelligent computer mathematics, AISC'10/MKM'10/Calculemus'10, pp.189-203, 2010.
DOI : 10.1007/978-3-642-14128-7_17
URL : https://hal.archives-ouvertes.fr/inria-00464237

C. Cohen and A. Mörtberg, A Coq Formalization of Finitely Presented Modules, Interactive Theorem Proving -5th International Conference, pp.193-208, 2014.
DOI : 10.1007/978-3-319-08970-6_13
URL : https://hal.archives-ouvertes.fr/hal-01378905

T. Coquand, A. Mörtberg, and V. Siles, Coherent and Strongly Discrete Rings in Type Theory, Certified Programs and Proofs, pp.273-288
DOI : 10.1007/978-3-642-35308-6_21

T. Coquand, A. Mörtberg, and V. Siles, A formal proof of Sasaki-Murao algorithm, Journal of Formalized Reasoning, vol.5, issue.1, p.2013

W. Decker and C. Lossen, Computing in Algebraic Geometry: A Quick Start using SINGULAR, 2006.

M. Dénès, A. Mörtberg, and V. Siles, A Refinement-Based Approach to Computational Algebra in Coq, Interactive Theorem Proving, pp.83-98, 2012.
DOI : 10.1007/978-3-642-32347-8_7

L. Fuchs and L. Salce, Modules Over Non-Noetherian Domains. Mathematical surveys and monographs, 2001.
DOI : 10.1090/surv/084

R. Gamboa, J. Cowles, and J. V. Baalen, Using ACL2 arrays to formalize matrix algebra, Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03), 2003.

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Proceedings 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs'09), pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, Interactive Theorem Proving, pp.103-118, 2011.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-00805966

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Greuel and G. Pfister, A Singular Introduction to Commutative Algebra, 2007.
DOI : 10.1007/978-3-662-04963-1

J. Harrison, The HOL Light Theory of Euclidean Space, Journal of Automated Reasoning, vol.4, issue.2, pp.173-190, 2013.
DOI : 10.1007/s10817-012-9250-9

A. Hatcher, Algebraic Topology, 2001.

O. Helmer, The elementary divisor theorem for certain rings without chain condition. Bulletin of the, pp.225-236, 1943.

J. Hendrix, Matrices in ACL2, Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 '03), 2003.

J. Heras, T. Coquand, A. Mörtberg, and V. Siles, Computing persistent homology within Coq/SSReflect, ACM Transactions on Computational Logic, vol.14, issue.4, pp.1-26, 2013.
DOI : 10.1145/2528929
URL : http://arxiv.org/abs/1209.1905

I. Kaplansky, Elementary divisors and modules. Transactions of the, pp.464-491, 1949.
DOI : 10.1090/s0002-9947-1949-0031470-3

H. Lombardi and C. Quitté, Algèbre commutative, Méthodes constructives: Modules projectifs de type fini, Calvage et Mounet, 2011.

D. Lorenzini, On Bézout Domains

H. Lüneburg, On a little but useful algorithm, Proceedings of the 3rd International Conference on Algebraic Algorithms and Error-Correcting Codes, AAECC-3, pp.296-301, 1986.
DOI : 10.1007/3-540-16776-5_732

N. Magaud, Programming with Dependent Types in Coq: a Study of Square Matrices, 2005.
URL : https://hal.archives-ouvertes.fr/hal-00955444

R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive Algebra, 1988.
DOI : 10.1007/978-1-4419-8640-5

B. Nordström, Terminating general recursion, BIT, vol.24, issue.3, pp.605-619, 1988.
DOI : 10.1007/BF01941137

S. Obua, Proving Bounds for Real Linear Programs in Isabelle/HOL, Lecture Notes in Computer Science, vol.3603, pp.227-244, 2005.
DOI : 10.1007/11541868_15

H. Perdry, Strongly Noetherian rings and constructive ideal theory, Journal of Symbolic Computation, vol.37, issue.4, pp.511-535, 2004.
DOI : 10.1016/j.jsc.2003.02.001
URL : http://doi.org/10.1016/j.jsc.2003.02.001

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

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

J. Stein, Documentation of my formalization of linear algebra, 2001.

J. Zeng, A bijective proof of Muir's identity and the Cauchy-Binet formula, Linear Algebra and its Applications, vol.184, issue.0, pp.79-82, 1993.
DOI : 10.1016/0024-3795(93)90371-T