Formalisation and execution of Linear Algebra: theorems and algorithms

Ponente: Jose Divasón Mallagaray (Universidad de La Rioja)

Lugar: Sala de Grados (Edificio CCT)

Hora: miércoles 15 de junio, 12:00

Resumen: This talk is about the formalisation and execution of Linear Algebra algorithms in Isabelle/HOL, an interactive theorem prover. The work is based on the HOL Multivariate Analysis library, whose matrix representation has been refined to datatypes that admit a representation in functional programming languages. This enables the generation of programs from such verified algorithms. In particular, several well-known Linear Algebra algorithms have been formalised involving both the computation of matrix canonical forms and decompositions (such as the Gauss-Jordan algorithm, echelon form, Hermite normal form, and QR decomposition). Some benchmarks of the generated programs are presented as well where matrices of remarkable dimensions are involved, illustrating the fact that they are usable in real-world cases. In addition, an experiment involving Isabelle, its logics, and the formalisation of some underlying mathematical concepts presented in Voevodsky’s simplicial model for Homotopy Type Theory is presented.

The presentation  is available through this link.

Nota: la charla se trata de una prueba de tiempo para la presentación de la Tesis, que tendrá lugar el día 20 de junio a las 16:00 en la misma Sala de Grados del CCT.