A Refinement-Based Approach to Computational Algebra in Coq
From MaRDI portal
Publication:2914734
DOI10.1007/978-3-642-32347-8_7zbMath1360.68745OpenAlexW1649228311MaRDI QIDQ2914734
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
A formalisation in HOL of the fundamental theorem of linear algebra and its application to the solution of the least squares problem ⋮ Formally-verified decision procedures for univariate polynomial computation based on Sturm's and Tarski's theorems ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL ⋮ Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation ⋮ Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory ⋮ A bi-directional extensible interface between Lean and Mathematica ⋮ The matrix reproved (verification pearl) ⋮ Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm ⋮ From Sets to Bits in Coq ⋮ A formalization of the Smith normal form in higher-order logic ⋮ Modelling algebraic structures and morphisms in ACL2 ⋮ Theorem of three circles in Coq ⋮ Formally verified certificate checkers for hardest-to-round computation
Uses Software
This page was built for publication: A Refinement-Based Approach to Computational Algebra in Coq
