Formalized linear algebra over Elementary Divisor Rings in Coq

Article, Preprint English OPEN
Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent;
(2016)
  • Publisher: Logical Methods in Computer Science Association
  • Related identifiers: doi: 10.2168/LMCS-12(2:7)2016
  • Subject: ACM: I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE/I.2.3: Deduction and Theorem Proving | Mathematics - Rings and Algebras | Computer Science - Logic in Computer Science | ACM : F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic | [MATH.MATH-RA]Mathematics [math]/Rings and Algebras [math.RA] | I.2.3 | [ INFO.INFO-LO ] Computer Science [cs]/Logic in Computer Science [cs.LO] | [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] | ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic | [ MATH.MATH-RA ] Mathematics [math]/Rings and Algebras [math.RA] | ACM : I.: Computing Methodologies/I.2: ARTIFICIAL INTELLIGENCE/I.2.3: Deduction and Theorem Proving | F.4.1
    acm: ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION

International audience; This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential o... View more
  • References (41)
    41 references, page 1 of 5

    [1] 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, 10(2):269{293, 2011.

    [2] M. Barakat and D. Robertz. homalg { A Meta-Package for Homological Algebra. Journal of Algebra and Its Applications, 7(3):299{317, 2008.

    [3] Y. Bertot, G. Gonthier, S. Biha, and I. Pasca. Canonical big operators. In Theorem Proving in HigherOrder Logics (TPHOLs'08), volume 5170 of LNCS, pages 86{101, 2008.

    [4] G. Cano and M. Denes. Matrices a blocs et en forme canonique. In D. Pous and C. Tasson, editors, JFLA - Journees francophones des langages applicatifs, Aussois, France, 2013. Damien Pous and Christine Tasson, Damien Pous and Christine Tasson.

    [5] C. Cohen, M. Denes, and A. Mortberg. Re nements for Free! In G. Gonthier and M. Norrish, editors, Certi ed Programs and Proofs, volume 8307 of Lecture Notes in Computer Science, pages 147{162. Springer International Publishing, 2013.

    [6] C. Cohen and A. Mahboubi. A formal quanti er elimination for algebraically closed elds. In Proceedings of the 10th ASIC and 9th MKM international conference, and 17th Calculemus conference on Intelligent computer mathematics, AISC'10/MKM'10/Calculemus'10, pages 189{203, Berlin, Heidelberg, 2010. Springer-Verlag.

    [7] C. Cohen and A. Mortberg. A Coq Formalization of Finitely Presented Modules. In Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria., pages 193{208. Springer, 2014.

    [8] Coq development team. The Coq Proof Assistant Reference Manual, version 8.4. Technical report, Inria, 2012.

    [9] T. Coquand, A. Mortberg, and V. Siles. Coherent and Strongly Discrete Rings in Type Theory. In C. Hawblitzel and D. Miller, editors, Certi ed Programs and Proofs, volume 7679 of Lecture Notes in Computer Science, pages 273{288. Springer Berlin Heidelberg, 2012.

    [10] T. Coquand, A. Mortberg, and V. Siles. A formal proof of Sasaki-Murao algorithm. Journal of Formalized Reasoning, 5(1), 2013.

  • Related Research Results (1)
  • Metrics
    No metrics available
Share - Bookmark