CoqEAL -- The Coq Effective Algebra Library
Coq Verilog Other
Clone or download
Latest commit 716acbc Jan 7, 2016
Failed to load latest commit information.
doc + coq2html (compcert) Feb 10, 2014
refinements adding specQ Jan 7, 2016
release 0.9.2 release Sep 15, 2014
theory minor fixes Nov 11, 2014
v0.1 Add the big matrix from the AMS paper Jan 27, 2015
.gitignore More in .gitignore. Apr 24, 2014 update README Feb 10, 2014 script to build releases Feb 10, 2014

CoqEAL - The Coq Effective Algebra Library

This repository contains a subset of the work that was developed in the context of the ForMath european project (2009-2013). This archive is split in four parts:

  • theory (package CoqEAL_theory), which contains formal developments in algebra.

  • refinements (package CoqEAL_refinements), which contains optimized algorithms with a framework to ease change of representation during a proof.

  • v0.1, a previous version of the framework, for archiving purpose.

  • doc, tools for generating documentation out of local documentation.


Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg and Vincent Siles.