Komendantskaya, Ekaterina; Heras, Jónathan Proof mining with dependent types. (English) Zbl 1367.68251 Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 303-318 (2017). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{E. Komendantskaya} and \textit{J. Heras}, Lect. Notes Comput. Sci. 10383, 303--318 (2017; Zbl 1367.68251) Full Text: DOI arXiv
Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico Modelling algebraic structures and morphisms in ACL2. (English) Zbl 1325.68214 Appl. Algebra Eng. Commun. Comput. 26, No. 3, 277-303 (2015). MSC: 68T15 68W30 PDFBibTeX XMLCite \textit{J. Heras} et al., Appl. Algebra Eng. Commun. Comput. 26, No. 3, 277--303 (2015; Zbl 1325.68214) Full Text: DOI Link
Poza, María; Domínguez, César; Heras, Jónathan; Rubio, Julio A certified reduction strategy for homological image processing. (English) Zbl 1354.68286 ACM Trans. Comput. Log. 15, No. 3, Article No. 23, 23 p. (2014). MSC: 68U10 03B35 55U15 68T15 92C55 PDFBibTeX XMLCite \textit{M. Poza} et al., ACM Trans. Comput. Log. 15, No. 3, Article No. 23, 23 p. (2014; Zbl 1354.68286) Full Text: DOI arXiv
Heras, Jónathan; Komendantskaya, Ekaterina Recycling proof patterns in Coq: case studies. (English) Zbl 1302.68243 Math. Comput. Sci. 8, No. 1, 99-116 (2014). MSC: 68T15 68T05 PDFBibTeX XMLCite \textit{J. Heras} and \textit{E. Komendantskaya}, Math. Comput. Sci. 8, No. 1, 99--116 (2014; Zbl 1302.68243) Full Text: DOI arXiv
Heras, Jónathan; Poza, María; Dénès, Maxime; Rideau, Laurence Incidence simplicial matrices formalized in Coq/SSReflect. (English) Zbl 1335.68229 Davenport, James H. (ed.) et al., Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18–23, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22672-4/pbk). Lecture Notes in Computer Science 6824. Lecture Notes in Artificial Intelligence, 30-44 (2011). MSC: 68T15 55-04 55U10 PDFBibTeX XMLCite \textit{J. Heras} et al., Lect. Notes Comput. Sci. 6824, 30--44 (2011; Zbl 1335.68229) Full Text: DOI Link