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. © 2010 Springer-Verlag Berlin Heidelberg.
Author supplied keywords
Cite
CITATION STYLE
Domínguez, C., & Rubio, J. (2010). Computing in Coq with infinite algebraic data structures. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6167 LNAI, pp. 204–218). https://doi.org/10.1007/978-3-642-14128-7_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
