Ponente: Fabian Immler (Technische Universität München)
Lugar: Seminario Mirian Andrés (Edificio CCT)
Hora: miércoles 15 de noviembre, 14:00
Resumen: In this talk, I will present which concepts and results from linear algebra are used in my verified rigorous numerical ODE solver. Instead of matrices I work with a type of bounded linear functions. Matrix operations are represented as (lists of) deeply embedded arithmetic expressions. I set up Lifting and Transfer to convert between the type class of Euclidean space and vectors or matrices.
The slides of the talk are available from the following link.