Research

A few publications and links to them:

• A formalisation in HOL of the Fundamental Theorem of Linear Algebra and its application to the solution of the least squares problem
  Aransay J., Divasón J.
  Accepted for publication in Journal of Automated Reasoning. 2016
  The final publication is available at http://link.springer.com.
• Formalisation of the computation of the Echelon Form of a matrix in Isabelle/HOL
  Aransay J., Divasón J.
  Accepted for publication in Formal Aspects of Computing. 2016
  The final publication is available at http://link.springer.com.
• Verified Computer Linear Algebra
  Aransay J., Divasón J.
  XVII Spanish Meeting on Computer Algebra and Applications (EACA 2016)
• Formalisation in Higher-Order Logic and code generation to functional languages of the Gauss-Jordan algorithm
  Aransay J., Divasón J.
  Journal of Functional Programming, Volume 25, e9, 1 - 21. 2015
  The final publication is available at Cambridge University Press.
• Generalizing a Mathematical Analysis library in Isabelle/HOL
  Aransay J., Divasón J.
  Proceedings of the Seventh NASA Formal Methods Symposium (NFM 2015)
  The final publication is available at http://link.springer.com
• Obtaining an ACL2 specification from an Isabelle/HOL theory
  Aransay J., Divasón J., Heras J., Lambán L., Pascual V., Rubio A.L. and Rubio J.
  Proceedings of the Artificial Intelligence and Symbolic Computation (AISC 2014)
  The final publication is available at http://link.springer.com
• Formalization and execution of Linear Algebra: from theorems to algorithms
  Aransay J., Divasón J.
  Revised Selected Papers of the Logic-Based Program Synthesis and Transformation (LOPSTR 2013)
  The final publication is available at http://link.springer.com
• Formalization and execution of Linear Algebra: from theorems to algorithms
  Aransay J., Divasón J.
  Proceedings of the Logic-Based Program Synthesis and Transformation (LOPSTR 2013)
• Performance Analysis of a Verified Linear Algebra Program in SML
  Aransay J., Divasón J.
  Proceedings of the XII Jornadas sobre Programación y Lenguajes (PROLE 2013) y V Taller de Programación
• Formalizing an abstract algebra textbook in Isabelle/HOL
  Aransay J., Divasón J.
  XIII Spanish Meeting on Computer Algebra and Applications (EACA 2012)
• Generating certified code from formal proofs: a case study in homological algebra
  Aransay J., Ballarin C., Rubio J.
  X Jornadas de Programación y Lenguajes, PROLE2010 (abstract).
• Generating certified code from formal proofs: a case study in homological algebra
  Aransay J., Ballarin C., Rubio J.
  Formal Aspects of Computing, Volume 22, number 2 (2010), Springer.
• Modelling Differential Structures in Proof Assistans: the Graded Case
  Aransay J., Domínguez C.
  12th International Conference on Computer Aided Systems Theory, EUROCAST2009, Springer.
• Mechanized Reasoning in Homological Algebra
  Aransay J.
  AI Communications, Volume 21, Number 4 (2008)
• Representation of graded structures in proof assistants
  Aransay J., Domínguez C.
  11º Encuentro de Álgebra Computacional y Aplicaciones, EACA2008
• A Mechanized Proof of the Basic Perturbation Lemma
  Aransay J., Ballarin C., Rubio J.
  Journal of Automated Reasoning, Volume 40, number 4 (2008), Springer.
• Mechanized Reasoning in Homological Algebra
  Aransay J.
  Ph.D. thesis (April, 2006)
• Extracting computer algebra programs from statements
  Aransay J., Ballarin C., Rubio J.
  10th International Conference on Computer Aided Systems Theory, EUROCAST2005, Springer.
• Four Approaches to Automated Reasoning with Differential Algebraic Structures
  Aransay J., Ballarin C., Rubio J.
  7th International Conference on Artificial Intelligence and Symbolic Computation, AISC2004, Springer.
• Towards a Higher Reasoning Level in Formalized Homological Algebra
  Aransay J., Ballarin C., Rubio J.
  Calculemus 2003
• Deduction and Computation in Algebraic Topology
  Aransay J., Ballarin C., Rubio J.
  I Taller Iberoamericano sobre Deducción Automática e Inteligencia Artificial
• Towards an Automated Proof of the Basic Perturbation Lemma
  Aransay J., Ballarin C., Rubio J.
  8º Encuentro de Álgebra Computacional y Aplicaciones, EACA2002
• Mechanizing Proofs in Homological Algebra
  Aransay J. Ballarin C., Rubio J.
  Calculemus Autumn School 2002
• Object Oriented Implementation of Algebraic Structures: a Case Study in Java and C++
  Aransay J., Olarte J.J., Rubio J.
  7º Encuentro de Álgebra Computacional y Aplicaciones, EACA2001

Some talks (more to come soon):

• Rendering useful formalized mathematics
  Thematic Program on Computer Algebra
  Workshop on Algebra, Geometry and Proofs in Symbolic Computation
  Fields Institute, Toronto, Canada. December, 7th - 16th. 2016.