Thesis: formal study of efficient algorithms in linear algebra

My thesis document is online.

It is written in French. If you cannot read French, you may want to read my publications covering much of the same material.

The defense took place on November 20, 1:30pm (CET) in Sophia-Antipolis (France), in the I3S lab near Inria.

The companion material to my thesis has not been packaged yet, but you can find most of it in a few places already.

The native compiler described in chapter 1 is implemented in Coq's trunk which you can access through SVN:
svn checkout svn://scm.gforge.inria.fr/svnroot/coq/trunk

Note that machine integers and persistent arrays have not been integrated yet, but can be found in an experimental branch called native-coq:
https://github.com/maximedenes/native-coq

The refinements framework described in chapter 2, as well as Strassen's algorithm (chapter 3), Gaussian elimination (chapter 4) and part of the development on canonical forms (chapter 5) can be found at:
http://www.maximedenes.fr/content/coqeal-coq-effective-algebra-library

I am working on packaging the remainder, especially the development on homology described in chapters 6 and 7.