Formalization and execution of linear algebra: from theorems to algorithms

DOI10.1007/978-3-319-14125-1_1MaRDI QIDQ3453644zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Jesús Aransay, Jose Divasón

Publication date 30 November 2015

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-14125-1_1

zbMATH Keywords

verificationlinear algebracode generation

Mathematics Subject Classification ID

Direct numerical methods for linear systems and matrix inversion (65F05) Biomedical imaging and signal processing (92C55) Formalization of mathematics in connection with theorem provers (68V20) Linear transformations, semilinear transformations (15A04)

Recommendations

• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• A formalization of the Smith normal form in higher-order logic
• Point-free, set-free concrete linear algebra

Cites work

• scientific article; zbMATH DE number 5162350 (Why is no real title available?)
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• A refinement-based approach to computational algebra in Coq
• A revision of the proof of the Kepler conjecture
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Automatic Data Refinement
• Code generation via higher-order rewrite systems
• Computing persistent homology within Coq/SSReflect
• Data refinement in Isabelle/HOL
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalizing Arrow's theorem
• Incidence simplicial matrices formalized in Coq/SSReflect
• Isabelle/HOL. A proof assistant for higher-order logic
• Light-weight containers for Isabelle: efficient, extensible, nestable
• The HOL Light theory of Euclidean space
• Theorem Proving in Higher Order Logics
• Towards a certified computation of homology groups for digital images
• Type classes and filters for mathematical analysis in Isabelle/HOL

Cited in

(10)

• Formal theories for linear algebra
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• scientific article; zbMATH DE number 7649964 (Why is no real title available?)
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Formal derivation of algorithms
• Point-free, set-free concrete linear algebra
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
• Modelling algebraic structures and morphisms in ACL2

Describes a project that uses

Uses Software

• Rank Nullity
• Gauss Jordan Elimination
• Gauss-Jordan
• Autoref
• Coq/SSReflect
• HOL
• Isabelle/HOL
• Isabelle

This page was built for publication: Formalization and execution of linear algebra: from theorems to algorithms

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453644)