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)

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

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)