Incidence Simplicial Matrices Formalized in Coq/SSReflect. - Jónathan Heras; María Poza; Maxime Dénès; Laurence Rideau (Calculemus/MKM, 2011)

Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging. - Jónathan Heras; María Poza; Julio Rubio 001 (AISC/MKM/Calculemus, 2012)

Towards a Certified Computation of Homology Groups for Digital Images. - Jónathan Heras; Maxime Dénès; Gadea Mata; Anders Mörtberg; María Poza; Vincent Siles (CTIC, 2012)

A Certified Reduction Strategy for Homological Image Processing. - María Poza; César Domínguez 001; Jónathan Heras; Julio Rubio 001 (ACM Trans. Comput. Log., 2014)