CoqEAL

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.