Publicaciones en las que colabora con 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

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