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.

The Perron-Frobenius Theorem in Isabelle/HOL — Transferring between Matrix-Representations

Ponente: René Thiemann (University of Innsbruck)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 15 de noviembre, 11:00

Resumen: Matrix interpretations are widely used in automated complexity analysis.
For these interpretations, certification boils down to
determining the growth rate of A^n for a fixed non-negative real
matrix A.

Since the direct approach to compute the growth rate of A
via algebraic numbers is quite slow, in this work we formalize
the Perron-Frobenius theorem: it permits us to avoid algebraic
numbers, so that our new certification algorithm only has to perform
simple arithmetic operations. To cover the theorem in its full extend,
we further establish a connection between two different Isabelle/HOL
libraries on matrices, which enables an easy exchange of theorems between
both libraries.

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

Inteligencia Artificial para Interpretar Mapas

Ponente: Jónathan Heras Vicente (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 4 de octubre, 11:00

Resumen: La segmentación semántica es una técnica de Inteligencia Artificial que tiene como objetivo el ser capaces de comprender una imagen al nivel de píxel, es decir ser capaces de otorgar una etiqueta o categoría a cada píxel de una imagen. Por ejemplo, en el caso que nos ocupa en esta charla, queremos ser capaces de distinguir en una imagen aérea los píxeles que pertenecen a edificaciones, a carreteras o que son considerados como fondo.

En esta charla, presentamos como las técnicas de aprendizaje profundo pueden ser aplicadas a la segmentación semántica y su aplicación a la detección de edificaciones y carreteras en imágenes aéreas disponibles en IDERioja.

Puedes acceder a las transparencias de la charla a través de este enlace.

Nota: el blog de la comunidad de la Infraestructura de Datos Espaciales de España  (IDEE) recoge en una entrada el contenido de la charla. Puedes acceder a la entrada en el siguiente enlace.

Mujeres en estudios de informática: lo que no te explican

 

Ponente: Eva Tobías Olarte (Doctora en Estudios de Género y Agente de Igualdad, http://www.estrategiaygenero.com)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: martes 12 de septiembre, 10:00

Resumen: Es un hecho que, hoy en día, las mujeres están escasamente representadas en el ámbito formativo y también profesional de las TIC. Es por ello que en este espacio nos preguntaremos si para las mujeres la tecnología es una «cosa de hombres», o si es que ellas rinden peor en asignaturas como las matemáticas. Abordar la perspectiva de género (y lo que ello implica) en la educación, nos permitirá matizar algunas respuestas, y por qué no, descubrir «lo que no te explican».

Processing Biomedical Images for the Study of Treatments Related to Neurodegenerative Diseases

 

Ponente: Gadea Mata Martínez (Universidad de La Rioja)

Lugar: Salón de Actos (Edificio CCT)

Hora: martes 5 de septiembre, 12:00

Resumen: The study of neuronal cell morphology and function in neurodegenerative disease processes is essential in order to develop suitable treatments. In fact, studies such as the quantification of either synapses or the neuronal density are instrumental in measuring the evolution and the behaviour of neurons under the effects of certain physiological conditions.

In order to analyse this data, fully automatic methods are required. To this end, we have studied and developed methods inspired by Computational Algebraic Topology and Machine Learning techniques. Notions such as the definition of connected components, or others related to the persistent homology and zigzag persistence theory have been used to compute the synaptic density or to recognise the neuronal structure. In addition, machine learning methods have been used to determine where neurons are located in large images and to ascertain which are the best features to describe this kind of cells.

Nota: la charla se trata de una prueba de tiempo para la presentación de la Tesis, que tendrá lugar el viernes 15 de septiembre a las 12:00 en el mismo Salón de Actos del CCT.

The poset of depolarizations of a square free monomial ideal

 

Ponente: Patricia Pascual Ortigosa

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: lunes 24 de julio, 12:00

Resumen: Polarization is an operation that transforms a monomial ideal of a polynomial ring R into a squarefree monomial ideal in another polynomial ideal S that shares several important features of the original ideal.  Polarization is used in a wide variety of applications in the theory of monomial ideals. The inverse operation, depolarization, has however been less studied. It can be used to study squarefree monomial ideals using general monomial ideals which is convenient in a variety of situations. Depolarization is not unique, and in this talk we study the set of all possible depolarizations of a given squarefree monomial ideal obtaining the equivalence classes of monomial ideals with the same polarization. For this, we define depolarization orders and depolarization posets and study the ideals in them.

Nota: la charla se trata de una prueba de tiempo de la conferencia del mismo título que la ponente impartirá en el 4º Congreso de Jóvenes Investigadores de la RSME que tendrá lugar en la Universitat de València del 4 al 8 de septiembre.

Functional Programming is Free

 

Ponente: Francis Sergeraert (Université Joseph Fourier – Grenoble 1)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: jueves 1 de junio, 12:00

Resumen: The Kenzo  program, devoted to Algebraic  Topology, uses intensively «Functional Programming».  The complexity  problem in such a situation must consider the *cost* of the numerous functional objects dynamically generated at runtime, with a structure rather complex. The underlying tool, the notion of «closure» is essential in the process. Good news: we will explain why, in our  context, the cost of these functional objects is essentially null. Needs a lucid understanding of the real structure of these magic objects called «closures», the main subject of the talk. No knowledge in Algebraic Topology is required to attend this talk.