Formalisations:

• Incidence simplicial matrices formalized in Coq/SSReflect. J. Heras, M. Poza, M. Dénès and L. Rideau.
• Lecture Notes in Computer Science, 6824, pages 30--44, 2011. Conference: CICM 2011
• Description:
  Simplicial complexes are at the heart of Computational Algebraic Topology, since they give an elementary description of finite objects. The whole theory is used in different contexts such as coding theory, robotics or digital image analysis. In this paper we present a formalization in the COQ theorem prover of simplicial complexes and their incidence matrices as well as the main theorem that gives meaning to the definition of homology groups and is a first step towards their computation.
• Code
• Paper (preprint)
• DOI

• Towards a certified computation of homology groups for digital images. J. Heras Heras, M. Dénès, G. Mata, A. Mörtberg, M. Poza, and V. Siles.
• Lecture Notes in Computer Science, 7309, pages 49--57, 2012. Conference: CTIC 2012
• Description:
  In this paper we report on a project to obtain a verified computation of homology groups of digital images. The methodology is based on programming and executing inside the Coq proof assistant. Though more research is needed to integrate and make efficient more processing tools, we present some examples partially computed in Coq from real biomedical images.
• Code
• Paper (preprint)
• DOI

• Verifying an algorithm computing Discrete Vector Fields for digital imaging, J. Heras, M. Poza, and J. Rubio.
• Lecture Notes in Computer Science, 7362, pages 215--229, 2012. Conference: Calculemus 2012
• Description:
  In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discrete vector fields are a tool which has been welcomed in the homological analysis of digital images since it provides a procedure to reduce the amount of information but preserving the homological properties. In particular, thanks to discrete vector fields, we are able to compute, inside Coq, homological properties of biomedical images which otherwise are out of the reach of this system.
• Code
• Paper (preprint)
• DOI

• Computing Persistent Homology within Coq/SSReflect. J. Heras, T. Coquand, A. Mörtberg, and V. Siles.
• ACM Transactions on Computational Logic, 14(4). 2013.
• Description:
  Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories
• Code
• Paper (Arxiv version)
• DOI


• A certified reduction strategy for homological image processing. M. Poza, C. Domínguez, J. Heras, and J. Rubio.
• ACM Transactions on Computational Logic, 15(3). 2014.
• Description:
  The analysis of digital images using homological procedures is an outstanding topic in the area of Computational Algebraic Topology. In this paper, we describe a certified reduction strategy to deal with digital images, but preserving their homological properties. We stress both the advantages of our approach (mainly, the formalisation of the mathematics allowing us to verify the correctness of algorithms) and some limitations (related to the performance of the running systems inside proof assistants). The drawbacks are overcome using techniques that provide an integration of computation and deduction. Our driving application is a problem in bioinformatics, where the accuracy and reliability of computations are specially requested.
• Code
• Paper (Arxiv version)
• DOI

• ACL2 verification of Kenzo simplicial sets. J. Heras, V. Pascual and J. Rubio
• Lecture Notes in Computer Science, 6824, pages 30--44, 2011. Conference: LOPSTR 2010
• Description:
  Kenzo is a Common Lisp system devoted to Algebraic Topology. Although Kenzo uses higher-order functional programming intensively, we show in this paper how the theorem prover ACL2 can be used to prove the correctness of first order fragments of Kenzo. More concretely, we report on the verification in ACL2 of the implementation of simplicial sets. By means of a generic instantiation mechanism, we achieve the reduction of the proving effort for each family of simplicial sets, letting ACL2 automate the routine parts of the proofs.
• Code
• Paper (preprint)
• DOI


• A certified module of Simplicial Complexes for the Kenzo system. J. Heras, V. Pascual and J. Rubio
• Conference: EUROCAST 2011
• Description:
  Kenzo is a Computer Algebra System devoted to Algebraic Topology, and written in the Common Lisp programming language. In this paper, we give the programs which allow us to work with simplicial complexes in the Kenzo system, besides a complete automated proof of the correctness of our programs is provided. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp.
• Code
• Paper (preprint)


• A certified module to study digital images with the Kenzo system. J. Heras, V. Pascual and J. Rubio
• Lecture Notes in Computer Science, 6927, pages 113--120, 2011
• Description:
  Kenzo is a Computer Algebra system devoted to Algebraic Topology, written in the Common Lisp programming language. In this paper, programs which allow us to analyze monochromatic digital images with the Kenzo system are presented. Besides a complete automated proof of the correctness of our programs is provided. The proof is carried out using ACL2, a system for proving properties of programs written in (a subset of) Common Lisp.
• Code
• Paper (preprint)
• DOI


• Mathematical structures in ACL2. J. Heras, F.J. Martín-Mateos and V. Pascual
• Submitted
• Description:
  In this paper, we provide a methodology allowing one to deal with mathematical structures in the ACL2 theorem prover. Namely, we cope with the representation of mathematical structures, the certifiation that an object fullls the axioms which characterize an algebraic structure and the generation of generic instances of a concrete structure. As a by-product, an ACL2 algebraic hierarchy has been obtained. Our framework has been tested with the definition of homol- ogy groups, an example coming from Homological Algebra which involves several notions related to Universal Algebra. The method presented in this paper means a great profit, with respect to a from scratch approach, when we work with complex mathematical structures.
• Code
• Paper (preprint)