Using abstract stobjs in ACL2 to compute matrix normal forms
type: Item
instance of: scholarly article
title: Using abstract stobjs in ACL2 to compute matrix normal forms
zbMATH Open document ID: 1484.68312
DOI: 10.1007/978-3-319-66107-0_23
author: Laureano Lambán
author: Francisco Jesús Martín-Mateos
author: Julio Rubio
author: José Luis Ruiz-Reina
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 15B36
Mathematics Subject Classification ID: 68P05
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 6821862
zbMATH Keywords: matrices
zbMATH Keywords: ACL2
zbMATH Keywords: abstract stobjs
zbMATH Keywords: matrix normal forms
describes a project that uses: ACL2
describes a project that uses: Coq/SSReflect
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 23
OpenAlex ID: W2750465938
cites work: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
cites work: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
cites work: Formalized linear algebra over Elementary Divisor Rings in Coq
cites work: Hermite Normal Form Computation Using Modulo Determinant Arithmetic
cites work: Point-Free, Set-Free Concrete Linear Algebra
cites work: Computing persistent homology within Coq/SSReflect
cites work: The Smith normal form
description: scientific article; zbMATH DE number 6821862