A Coq formalization of finitely presented modules

DOI10.1007/978-3-319-08970-6_13MaRDI QIDQ2879252zbMATH OpenOpenAlexFDO

Authors Cyril Cohen, Anders Mörtberg

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01378905/file/main.pdf

zbMATH Keywords

constructive algebraCoqformalization of mathematicshomological algebraSSReflect

Mathematics Subject Classification ID

Finite generation, finite presentability, normal forms (diamond lemma, term-rewriting) (16S15)

Recommendations

• Effective homology of bicomplexes, formalized in Coq
• Computing persistent homology within Coq/SSReflect
• A Modular Formalisation of Finite Group Theory
• Finite Groups Representation Theory with Coq
• Computing in Coq with infinite algebraic data structures

Cited in

(12)

• Invariants for the FoCaL language
• Experience implementing a performant category-theory library in Coq
• Computing persistent homology within Coq/SSReflect
• Point-free, set-free concrete linear algebra
• A Modular Formalisation of Finite Group Theory
• Computing in Coq with infinite algebraic data structures
• Finite Groups Representation Theory with Coq
• On the role of formalization in computational mathematics
• scientific article; zbMATH DE number 7566073 (Why is no real title available?)
• Integration of multiple formal matrix models in Coq
• Effective homology of bicomplexes, formalized in Coq
• Generating certified code from formal proofs: a case study in homological algebra

Describes a project that uses

Uses Software

• Coq
• Coq/SSReflect

This page was built for publication: A Coq formalization of finitely presented modules

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2879252)