[isabelle] AFP: new developments in linear algebra

I am happy to announce two new developments in the AFP: Echelon Form and QR Decomposition, both by Jose DivasÃn and JesÃs Aransay. I wonât repeat the abstracts here (they are rather technical), but this work represents very impressive progress in the area of computational linear algebra, including matrix operations for solving linear systems and many other applications. The authors have also taken great care, both in writing highly polished proofs and at setting up code generation yielding what appears to be impressive performance.



Itâs great to see work like this being done.

Larry Paulson

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.