Conectando Kenzo con SageMath

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

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: lunes 08 de julio, 12:00

Resumen: En esta charla mostraremos un trabajo conjunto con Julián Cuevas, Miguel Marco y Ana Romero en el que se está desarrollando una interfaz de Kenzo para SageMath. El trabajo permite comunicar ambos sistemas y realizar cálculos de topología algebraica en Sage (grupos de homología y homotopía) que antes no eran posibles.

Factorización de polinomios y algoritmos de reducción de bases de retículos

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

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 19 de abril, 13:00

Resumen: Aunque resulte sorprendente, la factorización de polinomios es algo relativamente reciente. La historia de la factorización polinómica comienza con Hermann Schubert quien en 1793 describió el primer algoritmo de factorización de polinomios. En esta charla presentaremos cómo son los algoritmos modernos de factorización de polinomios, analizando también su complejidad computacional y mostrando cada paso a seguir a la hora de factorizar un polinomio eficientemente. Finalmente, introduciremos la definición matemática de retículo junto con uno de los algoritmos más conocidos para simplificar bases, además de sus numerosas aplicaciones.

Java 1.8. ¿Puede la programación orientada a objetos ser funcional?

 

Ponentes: Jose Divasón, Jesús Aransay

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: martes 21 de marzo, 12:00

Resumen: en esta charla haremos una breve presentación de algunas de las características más relevantes de Java 1.8. En particular, nos centraremos en las nuevas propiedades del lenguaje que permiten usar en Java tanto expresiones lambda como «streams». La charla pretende ser una introducción a estas características por medio de ejemplos y casos de uso que permitan ilustrar su sintaxis.

Puedes encontrar las transparencias de la charla en el siguiente enlace.

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.