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.
Type de document :
Communication dans un congrès
5th International Conference, ITP 2014, Jul 2014, Vienna, Austria. pp.193 - 208, 2014, 〈10.1007/978-3-319-08970-6_13〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01378905
Contributeur : Cyril Cohen <>
Soumis le : mardi 11 octobre 2016 - 00:14:17
Dernière modification le : vendredi 24 novembre 2017 - 13:44:02
Document(s) archivé(s) le : jeudi 12 janvier 2017 - 13:17:03

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

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, 2014, 〈10.1007/978-3-319-08970-6_13〉. 〈hal-01378905〉

Partager

Métriques

Consultations de la notice

71

Téléchargements de fichiers

23