Four Approaches to Automated Reasoning with Differential Algebraic Structures. - Jesús Aransay; Clemens Ballarin; Julio Rubio 001 (AISC, 2004)

Extracting Computer Algebra Programs from Statements. - Jesús Aransay; Clemens Ballarin; Julio Rubio 001 (EUROCAST, 2005)

Mechanized reasoning in Homological Algebra. - Jesús Aransay (AI Commun., 2008)

A Mechanized Proof of the Basic Perturbation Lemma. - Jesús Aransay; Clemens Ballarin; Julio Rubio 001 (J. Autom. Reason., 2008)

Modelling Differential Structures in Proof Assistants: The Graded Case. - Jesús Aransay; César Domínguez 001 (EUROCAST, 2009)

Generating certified code from formal proofs: a case study in homological algebra. - Jesús Aransay; Clemens Ballarin; Julio Rubio 001 (Formal Aspects Comput., 2010)

A case-study in algebraic manipulation using mechanized reasoning tools. - Jesús Aransay; César Domínguez 001 (Int. J. Comput. Math., 2010)

Formalization and Execution of Linear Algebra: From Theorems to Algorithms. - Jesús Aransay; Jose Divasón (LOPSTR, 2013)

Rank-Nullity Theorem in Linear Algebra. - Jose Divasón; Jesús Aransay (Arch. Formal Proofs, 2013)

Obtaining an ACL2 Specification from an Isabelle/HOL Theory. - Jesús Aransay-Azofra; Jose Divasón; Jónathan Heras; Laureano Lambán; María Vico Pascual; Ángel Luis Rubio; Julio Rubio 001 (AISC, 2014)

Gauss-Jordan Algorithm and Its Applications. - Jose Divasón; Jesús Aransay (Arch. Formal Proofs, 2014)

Applications of the Gauss-Jordan algorithm, done right. - Jesús Aransay; Jose Divasón (CoRR, 2014)

Generalizing a Mathematical Analysis Library in Isabelle/HOL. - Jesús Aransay; Jose Divasón (NFM, 2015)

QR Decomposition. - Jose Divasón; Jesús Aransay (Arch. Formal Proofs, 2015)

Echelon Form. - Jose Divasón; Jesús Aransay (Arch. Formal Proofs, 2015)

Hermite Normal Form. - Jose Divasón; Jesús Aransay (Arch. Formal Proofs, 2015)

Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm. - Jesús Aransay; Jose Divasón (J. Funct. Program., 2015)

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL. - Jesús Aransay; Jose Divasón (Formal Aspects Comput., 2016)

A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem. - Jesús Aransay; Jose Divasón (J. Autom. Reason., 2017)

A Formal Proof of the Computation of Hermite Normal Form in a General Setting. - Jose Divasón; Jesús Aransay (AISC, 2018)

Simplicial Complexes and Boolean functions. - Jesús Aransay; Alejandro del Campo; Julius Michaelis (Arch. Formal Proofs, 2021)

Formalizing Alexander duality through BDDs. - Jesús Aransay; Laureano Lambán; Julius Michaelis; Julio Rubio 001 (ISAIM, 2022)

Evasiveness Through Binary Decision Diagrams. - Jesús Aransay; Laureano Lambán; Julio Rubio 001 (CICM, 2023)