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

DOI10.1007/s00165-016-0383-1zbMath1348.68213OpenAlexW2471798638MaRDI QIDQ333325

Jesús Aransay, Jose Divasón

Publication date: 28 October 2016

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-016-0383-1

zbMATH Keywords

theorem provinglinear algebraIsabelle/HOLverified code generation

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Canonical forms, reductions, classification (15A21)

Related Items

A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formal analysis of the kinematic Jacobian in screw theory ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Using abstract stobjs in ACL2 to compute matrix normal forms ⋮ A Formal Proof of the Computation of Hermite Normal Form in a General Setting ⋮ Formalization of functional variation in HOL Light ⋮ Echelon Form ⋮ A formalization of the Smith normal form in higher-order logic

Uses Software

• ACL2
• Isabelle
• Isabelle/HOL
• Mizar
• Poly/ML
• seL4
• Transfer
• Lifting
• kepler98
• Cayley-Hamilton
• Gauss-Jordan
• QR Decomposition
• Jordan Normal Forms
• Archive Formal Proofs

Cites Work

• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Commutative algebra in the Mizar system
• Computation of approximate polynomial GCDs and an extension
• The HOL Light theory of Euclidean space
• A Refinement-Based Approach to Computational Algebra in Coq
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Refinements for Free!
• Animating the Formalised Semantics of a Java-Like Language
• Formalization and Execution of Linear Algebra: From Theorems to Algorithms
• Fast parallel matrix and GCD computations
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Formalized linear algebra over Elementary Divisor Rings in Coq
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL