CoqEAL - The Coq Effective Algebra Library. Cyril Cohen, Anders Mörtberg (University of Gothenburg) and I are currently developing a Coq library for effective algebra, by which we mean formally verified computer algebra algorithms that can be run inside Coq on concrete inputs. We designed a methodology based on refinements which allows us to prove the correctness of our algorithms on a proof-oriented description taking advantage of the SSReflect library, and then refine it to an efficient computation-oriented version. The proofs are transported mostly automatically using ideas found in the proof of the parametricity theorem for functional programming languages.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element