A Coq formalization of finitely presented modules

DOI10.1007/978-3-319-08970-6_13zbMATH Open1416.68157OpenAlexW1044853446MaRDI QIDQ2879252FDOQ2879252

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

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

zbMATH Keywords

homological algebraCoqformalization of mathematicsconstructive algebraSSReflect

Mathematics Subject Classification ID

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

Cited In (12)

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

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)