Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
type: Item
instance of: scholarly article
title: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
zbMATH Open document ID: 1348.68213
author: Jesús Aransay
author: Jose Divasón
published in: Formal Aspects of Computing
publication date: 2016-10-28T00:00:00Z
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 15A21
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 6645314
zbMATH Keywords: theorem proving
zbMATH Keywords: Isabelle/HOL
zbMATH Keywords: linear algebra
zbMATH Keywords: verified code generation
describes a project that uses: Mizar
describes a project that uses: seL4
describes a project that uses: Lifting
describes a project that uses: Transfer
describes a project that uses: ACL2
describes a project that uses: Isabelle
describes a project that uses: Archive Formal Proofs
describes a project that uses: Isabelle/HOL
describes a project that uses: Poly/ML
describes a project that uses: kepler98
describes a project that uses: Cayley-Hamilton
describes a project that uses: Gauss-Jordan
describes a project that uses: QR Decomposition
describes a project that uses: Jordan Normal Forms
MaRDI profile type: Publication
full work available at URL: s00165-016-0383-1
OpenAlex ID: W2471798638
cites work: Formalization and Execution of Linear Algebra: From Theorems to Algorithms
cites work: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
cites work: Q4827633
cites work: Fast parallel matrix and GCD computations
cites work: Q4831098
cites work: Formalized linear algebra over Elementary Divisor Rings in Coq
cites work: Refinements for Free!
cites work: A Refinement-Based Approach to Computational Algebra in Coq
cites work: Q4513600
cites work: Commutative algebra in the Mizar system
cites work: The HOL Light theory of Euclidean space
cites work: Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
cites work: Q4771385
cites work: Animating the Formalised Semantics of a Java-Like Language
cites work: Q4517538
cites work: Q3224016
cites work: Q5668937
cites work: Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
cites work: Computation of approximate polynomial GCDs and an extension
cites work: Q5195247
cites work: Q5847989
cites work: Q5743906
DOI: 10.1007/S00165-016-0383-1
description: scientific article; zbMATH DE number 6645314