Computing in Coq with infinite algebraic data structures

  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

Libro:
Proceedings CICM 2010

ISBN: 978-3-642-14127-0

Año de publicación: 2010

Volumen: 6167 LNAI

Páginas: 204-218

Tipo: Capítulo de Libro

DOI: 10.1007/978-3-642-14128-7_18 SCOPUS: 2-s2.0-77954880211 WoS: WOS:000286842300018 arXiv: 1004.4998 GOOGLE SCHOLAR lock_openAcceso abierto editor
Repositorio institucional: lockAcceso abierto Editor

Proyectos relacionados

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

2009/00207/001

Resumen

Computational content encoded into constructive type theory proofs can be used to make computing experiments over concrete data structures. In this paper, we explore this possibility when working in Coq with chain complexes of infinite type (that is to say, generated by infinite sets) as a part of the formalization of a hierarchy of homological algebra structures. © 2010 Springer-Verlag Berlin Heidelberg.