Jónathan Heras

Jónathan Heras Vicente

Despacho 3210. CCT. Department of Mathematics and Computer Science. University of La Rioja.

Logroño. Spain. 26004.

phone: (+34) 941299455

mail: joheras at gmail.com

Conferences:

J. Heras, M. Poza, C. Domínguez, and J. Rubio A Formal Proof of the Basic Perturbation Lemma. Seventh de Brún Workshop on Homological Perturbation Theory. Galway (Ireland), 2014.
M. Poza, C. Domínguez, J. Heras, and J. Rubio A Certified Reduction Strategy for Homological Image Processing. XIV Jornadas sobre Programación y Lenguajes (PROLE 2014). Cádiz (Spain), 2014.
J. Heras and E. Komendantskaya ACL2(ml): Machine-Learning for ACL2. 12th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2014). Vienna (Austria), 2014.
J. Heras and E. Komendantskaya Statistical Machine Learning in Interactive Theorem Proving. Coq workshop (Coq-6). Vienna (Austria), 2014.
J. Heras, E. Komendantskaya, M. Johansson, and E. Maclean Proof-Pattern Recognition and Lemma Discovery in ACL2. Scottish Theorem Proving seminar. St Andrews (UK), 2014.

J. Heras and E. Komendantskaya ML4PG in Computer Algebra Verification. CICM'2013. Bath (UK), 2013.
J. Heras, G. Mata, A. Romero, J. Rubio, and R. Saenz. Verifying a platform for digital imaging: a multi-tool strategy. CICM'2013 (Calculemus track). Bath (UK), 2013.
E. Komendantskaya and J. Heras. Statistical Machine Learning for Theorem Proving: Automated or Interactive?. 20th Automated Reasoning Workshop (ARW 2013), Dundee (UK), 2013.
J. Heras. ¿Pueden los ordenadores ayudarnos en la demostración de teoremas? (in Spanish) Invited talk at Seminario de Actualización en Matemáticas, University of La Rioja (20 March 2013).

K. Komendantskaya and J. Heras. ML4PG: Machine Learning for Proof General: interfacing interfaces. A talk given at the Universities of Stratchclyde (30 November 2012) and Edinburgh (4 December 2012).
J. Heras, G. Mata, and J. Rubio. Neuronal structure detection using persistent homology. Invited talk, Chalmers University, Goteborg (Sweden), 2012.
J. Heras, V. Pascual and F. J. Martín-Mateos. An ACL2 formalization of Algebraic Structures. XIII Encuentros de Álgebra Computacional y Aplicaciones (EACA 2012), Alcala de Henares (Spain), 2012.
J. Heras, M. Dénès, G. Mata, A. Mörtberg, M. Poza, and V. Siles. Towards a certified computation of homology groups for digital images. CTIC'2012, Bertinoro (Italy), 2012.
J. Heras, M. Poza and J. Rubio. Verifying an algorithm computing Discrete Vector Fields for digital imaging. CICM'2012. Bremen (Germany), 2012.
J. Heras, Some Notes about simplicial complexes and homology Part I, Part II. Computability of Homology groups. Formath junior meeting, Institute INRIA-Sophia (France), 2012.

J. Heras, G. Mata and M. Poza. Homological processing of biomedical images (in Spanish). Invited talk, Universidad de Valladolid (Spain), 2011.
J. Heras, G. Mata and M. Poza. Computational Algebraic Topology for biomedical imaging (in Spanish). Pearl award in AICA'2011, Granada (Spain), 2011.
J. Heras, V. Pascual and J. Rubio. A certified module to study digital images with the Kenzo system. EUROCAST'2011, Las Palmas de Gran Canaria (Spain), 2011.
J. Heras, V. Pascual and J. Rubio. A System for Computing and Reasoning in Algebraic Topology. CICM'2011, Bertinoro (Italy), 2011.
J. Heras, M. Poza, M. Dénès and L. Rideau. Incidence simplicial matrices formalized in Coq/SSReflect. CICM'2011, Bertinoro (Italy), 2011.
J. Heras, G. Mata, M. Poza and J. Rubio. Homological processing of biomedical digital images: automation and certification. Computer Algebra in Algebraic Topology and its Applications Session of ACA 2011 conference , Houston (USA), 2011.

J. Heras. Symbolic Computation tools for Algebraic Topology: effective homology (in Spanish) Encuentros de Topologia de datos, Santiago de Compostela (Spain), 2010.
J. Heras. fKenzo: a user interface for computations in Algebraic Topology Invited Seminar, University of Seville (Spain), 2010.
J. Heras and M. Poza. Incidence Simplicial Matrices on SSReflect. Invited talk in INRIA-Sophia institute (France), 2010.
J. Heras. An OpenMath Content Dictionary editor. Content Math Training Camp, Paris (France), 2010.
J. Heras. Symbolic Computation in Algebraic Topology. Doctoral Programme of Conferences on Intelligent Computer Mathematics, Paris (France), 2010.
J. Heras, V. Pascual, A. Romero and J. Rubio. Integrating multiple sources to answer questions in Algebraic Topology. 9th International Conference on Mathematical Knowledge Management (MKM 2010), Paris (France), 2010.
J. Heras, V. Pascual and J. Rubio. Proving with ACL2 the correctness of simplicial sets in the Kenzo system. 20th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2010), Hagenberg (Austria) 2010.
J. Heras and V. Pascual. ACL2 verification of Simplicial Complexes programs for the Kenzo system. Algebraic computing, soft computing, and program verification workshop, Castro Urdiales (Spain), 2010.
J. Heras. Effective Homology of the pushout of simplicial sets. XII Encuentros de Álgebra Computacional y Aplicaciones (EACA 2010), Santiago de Compostela (Spain), 2010.

J. Heras. fKenzo: a user interface for computations in Algebraic Topology. Invited Seminar, DFKI institute, Saarbrucken (Germany), 2009.
J. Heras, J. Rubio, L. J. Hernández, M. T. Rivas and E. Sáenz de Cabezón. Cálculo en paralelo de la homología cúbica con gridMathematica. III Congreso Mathematica España, Salamanca (Spain), 2009.
J. Heras, V. Pascual and J. Rubio. A customizable GUI through an OMDoc documents repository. Mathematical User-Interfaces workshop, Grand-Bend (Canada), 2009.
J. Heras, V. Pascual and J. Rubio. Using Open Mathematical Documents to Interface Computer Algebra and Proof Assistant Systems. 8th International Conference on Mathematical Knowledge Management (MKM 2009), Grand-Bend (Canada), 2009.
J. Heras, V. Pascual, J. Rubio. Content Dictionaries for Algebraic Topology. 22nd OpenMath Workshop, Grand-Bend (Canada), 2009.
J. Heras, V. Pascual, J. Rubio. Applying Generative Communication to Symbolic Computation in Common Lisp. 2nd European Lisp Symposium (ELS 2009), Milan (Italy), 2009.

J. Heras, V. Pascual, J. Rubio. A graphical user interface for the Kenzo system, a program to compute in Algebraic Topology. XI Encuentros de Álgebra Computacional y Aplicaciones (EACA 2008), Granada (Spain), 2008.
J. Heras, V. Pascual, J. Rubio and F. Sergeraert. Improving the usability of Kenzo, a Common Lisp system for Algebraic Topology. 1st European Lisp Symposium (ELS 2008), Bordeaux (France), 2008.