This paper presents a formalization of constructive module theory in the intuitionistic type theory of Coq. We build an abstraction layer on top of matrix encodings, in order to represent finitely presented modules, and obtain clean definitions with short proofs justifying that it forms an abelian category. The goal is to use it as a first step to get certified programs for computing topological invariants, like homology groups and Betti numbers. © 2014 Springer International Publishing.
CITATION STYLE
Cohen, C., & Mörtberg, A. (2014). A Coq formalization of finitely presented modules. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8558 LNCS, pp. 193–208). Springer Verlag. https://doi.org/10.1007/978-3-319-08970-6_13
Mendeley helps you to discover research relevant for your work.