A refinement-based approach to computational algebra in Coq

DOI10.1007/978-3-642-32347-8_7MaRDI QIDQ2914734zbMATH OpenOpenAlexFDO

Authors Maxime Dénès, Anders Mörtberg, Vincent Siles

Publication date 20 September 2012

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-00734505/file/coqeal.pdf

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)

Recommendations

• Refinements for free!
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• A verified implementation of algebraic numbers in Isabelle/HOL
• scientific article; zbMATH DE number 1303350
• Artificial Intelligence and Symbolic Computation

Cited in

(26)

• Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
• A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem
• Theorem of three circles in Coq
• Formally verified certificate checkers for hardest-to-round computation
• A formal method for developing algebraic and numerical algorithms
• Theorem Proving in Higher Order Logics
• The Picard Algorithm for Ordinary Differential Equations in Coq
• Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems
• Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
• Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
• Modelling algebraic structures and morphisms in ACL2
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• A certified program for the Karatsuba method to multiply polynomials
• A bi-directional refinement algorithm for the calculus of (co)inductive constructions
• Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
• Improving Real Analysis in Coq: A User-Friendly Approach to Integrals and Derivatives
• A verified implementation of algebraic numbers in Isabelle/HOL
• Formalization and execution of linear algebra: from theorems to algorithms
• Embedding of Systems of Affine Recurrence Equations in Coq
• Refinements for free!
• A formalization of the Smith normal form in higher-order logic
• A bi-directional extensible interface between Lean and Mathematica
• From Sets to Bits in Coq
• The matrix reproved (verification pearl)
• Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials
• scientific article; zbMATH DE number 1670755 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq

This page was built for publication: A refinement-based approach to computational algebra in Coq

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