Effective homology of bicomplexes, formalized in Coq

  1. Domínguez, C. 1
  2. Rubio, J. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

Revista:
Theoretical Computer Science

ISSN: 0304-3975

Año de publicación: 2011

Volumen: 412

Número: 11

Páginas: 962-970

Tipo: Artículo

DOI: 10.1016/J.TCS.2010.11.016 SCOPUS: 2-s2.0-79551482069 WoS: WOS:000287791400002 GOOGLE SCHOLAR

Otras publicaciones en: Theoretical Computer Science

Repositorio institucional: lock_openAcceso abierto Editor

Proyectos relacionados

Gestión Mecanizada del Conocimiento Matemático. Aplicaciones en Topología Algebraica y en Lógica.

2009/00207/001

Resumen

In this paper, we present a complete formalization in the Coq theorem prover of an important algorithm in computational algebra, namely the calculation of the effective homology of a bicomplex. As a necessary tool, we encode a hierarchy of algebraic structures in constructive type theory, including graded and infinite data structures. The experience shows how some limitations of the Coq proof assistant to deal with this kind of algebraic data can be overcome by applying a separation of concerns principle; more concretely, we propose to distinguish in the representation of an algebraic structure (such as a group or a module) a behavioural part, containing operation signatures and axioms, and a structural part determining if the algebraic data is free, of finite type and so on. © 2010 Elsevier B.V. All rights reserved.