Computing in Coq with infinite algebraic data structures
-
1
Universidad de La Rioja
info
ISBN: 978-3-642-14127-0
Argitalpen urtea: 2010
Alea: 6167 LNAI
Orrialdeak: 204-218
Mota: Liburuko kapitulua
Lotura duten proiektuak
Laburpena
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.