Publications dans lesquelles il/elle collabore avec Jesús María Aransay Azofra (19)

2018

  1. A formal proof of the computation of hermite normal form in a general setting

    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

  2. Towards a verified smith normal form algorithm in isabelle/hol

    Monografías de la Real Academia de Ciencias Exactas, Físicas, Químicas y Naturales de Zaragoza, Núm. 43, pp. 43-46

2017

  1. A Formalisation in HOL of the Fundamental Theorem of Linear Algebra and Its Application to the Solution of the Least Squares Problem

    Journal of Automated Reasoning, Vol. 58, Núm. 4, pp. 509-535

2016

  1. Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

    Formal Aspects of Computing, Vol. 28, Núm. 6, pp. 1005-1026

  2. Verified Computer Linear Algebra

    XV Encuentro de Álgebra computacional y aplicaciones: EACA 2016

2015

  1. Echelon Form

    Archive of Formal Proofs, Vol. 2015, pp. 1-171

  2. Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

    Journal of Functional Programming, Vol. 25, Núm. 1, pp. 1-21

  3. Generalizing a mathematical analysis library in Isabelle/HOL

    Lecture Notes in Computer Science, Vol. 9058, pp. 415-421

  4. Hermite Normal Form

    Archive of Formal Proofs, Vol. 2015, pp. 1-54

  5. QR Decomposition

    Archive of Formal Proofs, Vol. 2015, pp. 1-101

2014

  1. Formalization and execution of Linear Algebra: from theorems to algorithms

    Revised Selected Papers of the Logic-Based Program Synthesis and Transformation (LOPSTR 2013) (Springer), pp. 1-18

  2. Formalization and execution of linear algebra: From theorems to algorithms

    Lecture Notes in Computer Science, Vol. 8901, pp. 1-18

  3. Gauss-Jordan algorithm and its applications

    Archive of Formal Proofs, Vol. 2015, pp. 1-270

  4. Informática para las Matemáticas, Matemáticas para la Informática, Informática Aplicada

    Zubía, Núm. 26, pp. 19-37

  5. Obtaining an ACL2 specification from an Isabelle/HOL theory

    Lecture Notes in Computer Science, Vol. 8884, pp. 49-63

  6. Obtaining an ACL2 sprecification from an Isabelle/HOL theory

    Lecture Notes in Artificial Intelligence. Proceedings of AISC 2014 (Springer), pp. 49-63

2013

  1. Performance Analysis of a Verified Linear Algebra Program in SML

    Taller de Programación Funcional - XII Spanish Conference on Programming and Computer Languages, PROLE 2013, pp. 28-35

  2. Rank-Nullity Theorem in Linear Algebra

    Archive of Formal Proofs, pp. 1-9

2012

  1. Formalizing an abstract algebra textbook in Isabelle/HOL

    Libro de Resúmenes del XIII Encuentro de Álgebra Computacional y Aplicaciones: EACA 2012