Events

3 May 2012

Bldg I, 1st floor
Microsoft Research - Inria Joint Centre
Parc Orsay Université

Effective algebra with Coq and SSReflect
Maxime Dénès (Marelle research team)
Inria Sophia-Antipolis

Proof assistants like Coq provide a unified framework to describe the implementation of algorithms and their proofs of correctness. Using such a tool to formalize computer algebra algorithms seems a natural idea, but can be tricky because of the antagonism between rich proof-oriented datastructures and efficient computation-oriented implementations. We will describe a step-by-step software engineering methodology to work around this issue, and illustrate on a few examples like Winograd’s fast matrix product and the homology of digital images.

Finally, we will show how the construction of computable algebraic structures can be iterated, for instance in order to build effective matrices of effective polynomials. This opens the way for the verification and implementation of Frobenius and Jordan normal forms, which is ongoing work.