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
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Mahboubi, Assia; Sibut-Pinote, Thomas: A formal proof of the irrationality of (\zeta(3)) (2021)
- Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in \textscCoq (2016)
- Poza, María; Domínguez, César; Heras, Jónathan; Rubio, Julio: A certified reduction strategy for homological image processing (2014)
- Heras, Jónathan; Komendantskaya, Ekaterina: ML4PG in computer algebra verification (2013)
- Coquand, Thierry; Mörtberg, Anders; Siles, Vincent: A formal proof of Sasaki-Murao algorithm (2012)
Further publications can be found at: http://www.maximedenes.fr/publications