Computing in Coq with Infinite Algebraic Data Structures
Logic in Computer Science
2010-04-29 v1
Abstract
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.
Cite
@article{arxiv.1004.4998,
title = {Computing in Coq with Infinite Algebraic Data Structures},
author = {César Domínguez and Julio Rubio},
journal= {arXiv preprint arXiv:1004.4998},
year = {2010}
}
Comments
To appear in Conferences on Intelligent Computer Mathematics 2010