Semi-Automatic Asymptotics in Isabelle/HOL


Ponente: Manuel Eberl (Technische Universität München)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 16 de noviembre, 11:00

Resumen: Computer Algebra Systems can easily compute limits and asymptotic expansions of complicated real functions; interactive theorem provers, on the other hand, provide very little support for such problems and proving asymptotic properties of a function often involves long and tedious manual proofs. In this talk, I will present my work about bringing automation for real-valued asymptotics to Isabelle/HOL using multiseries expansions. This yields a procedure to automatically prove limits and ‘Big-O’ estimates of real-valued functions similarly to computer algebra systems like Mathematica and Maple – but while proving every step of the process correct.

The slides of the talk are available in the following link.

Recent development in Lean and its analysis


Ponente: Johannes Hölzl (Vrije Universiteit Amsterdam)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 16 de noviembre, 09:00

Resumen: I will present the current state of analysis in Lean 3. The formalization of the reals is based on the completion of uniform spaces, requiring a more extensive filter library. While the analysis in Lean is developed up to the Lebesgue measure, I mostly want to focus on topological spaces and measurable spaces, and compare their formalization with the one in Isabelle.

The slides of the talk are available from the following link.

Rigorous Numerics and Linear Algebra in Isabelle/HOL


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.

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.

Rendering useful formalized mathematics, with an application to image processing


Ponente: Jesús Aransay (Universidad de La Rioja)

Lugar: Seminario Chicho (Aula 314, Edificio Vives)

Hora: miércoles 9 de diciembre, 12:00

La charla está dentro de la “Bioimaging week” dedicada a distintos aspectos de la investigación en el procesamiento de imágenes biomédicas

Se trata de una prueba de tiempo para el Thematic Program in Computer Algebra que se celebra en Toronto entre Junio y Diciembre