A Coq Formalization of Finitely Presented Modules

Abstract : 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.
Complete list of metadatas

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-01378905
Contributor : Cyril Cohen <>
Submitted on : Tuesday, October 11, 2016 - 12:14:17 AM
Last modification on : Friday, November 24, 2017 - 1:44:02 PM
Long-term archiving on : Thursday, January 12, 2017 - 1:17:03 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Cyril Cohen, Anders Mörtberg. A Coq Formalization of Finitely Presented Modules. 5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.193 - 208, ⟨10.1007/978-3-319-08970-6_13⟩. ⟨hal-01378905⟩

Share

Metrics

Record views

101

Files downloads

113