A refinement-based approach to computational algebra in Coq
From MaRDI portal
Publication:2914734
DOI10.1007/978-3-642-32347-8_7zbMATH Open1360.68745OpenAlexW1649228311MaRDI QIDQ2914734FDOQ2914734
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
Recommendations
Symbolic computation and algebraic computation (68W30) Abstract data types; algebraic specification (68Q65)
Cited In (26)
- 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_4\) algorithm in Isabelle/HOL
- Title not available (Why is that?)
- 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
- Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL
- 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!
- The Picard Algorithm for Ordinary Differential Equations in Coq
- A bi-directional refinement algorithm for the calculus of (co)inductive constructions
Uses Software
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)
