Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

DOI10.1017/S0956796815000155MaRDI QIDQ5371950zbMATH OpenDBLPWikidataFDO

Authors Jesús Aransay, Jose Divasón

Publication date 23 October 2017

Published in Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/S0956796815000155

Mathematics Subject Classification ID

Direct numerical methods for linear systems and matrix inversion (65F05) Functional programming and lambda calculus (68N18)

Recommendations

• Formalization and execution of linear algebra: from theorems to algorithms
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Generating certified code from formal proofs: a case study in homological algebra
• A formalization of the Smith normal form in higher-order logic
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting

Cites work

• A refinement-based approach to computational algebra in Coq
• Code generation via higher-order rewrite systems
• Data refinement in Isabelle/HOL
• Formalization and execution of linear algebra: from theorems to algorithms
• scientific article; zbMATH DE number 5162350 (Why is no real title available?)
• scientific article; zbMATH DE number 5708645 (Why is no real title available?)
• Imperative Functional Programming with Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Proof pearl: A mechanized proof of GHC's mergesort
• Refinements for free!
• The HOL Light theory of Euclidean space
• The misfortunes of a trio of mathematicians using computer algebra systems. Can we trust in them?
• Theorem Proving in Higher Order Logics
• Towards a certified computation of homology groups for digital images

Cited in

(9)

• Using abstract stobjs in ACL2 to compute matrix normal forms
• A formalization of the Smith normal form in higher-order logic
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Gaussian elimination: a case study in efficient genericity with MetaOCaml
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Formalization and execution of linear algebra: from theorems to algorithms
• A formal proof of Sasaki-Murao algorithm
• A Formal Proof of the Computation of Hermite Normal Form in a General Setting
• Generating certified code from formal proofs: a case study in homological algebra

Describes a project that uses

Uses Software

• HOL Light
• Isabelle/HOL
• HOL
• Poly/ML
• kepler98
• Gauss-Jordan
• Isabelle
• ML
• Haskell
• CAVA LTL Modelchecker

This page was built for publication: Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm

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