Desarrollo de Cesens®: de la idea al mercado

 

Ponente: Carlos Acedo (Computer Engineer, Encore Lab)

Lugar: Seminario Mirian Andrés (Edificio CCT)

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

Resumen: Retrospectiva de los hitos y aspectos técnicos más relevantes de Cesens®, el sistema de monitorización de cultivos desarrollado por la empresa riojana Encore Lab, desde la concepción del proyecto hasta su lanzamiento al mercado. Se repasarán las tecnologías hardware y software en las que se basa el sistema, así como los principales problemas y soluciones que se dieron a lo largo del desarrollo.

An Isabelle/HOL formalisation of Green’s Theorem

 

Ponente: Mohammad Abdulaziz (Technische Universität München)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: viernes 17 de noviembre, 11:00

Resumen: We describe a formalisation of Green’s theorem, a fundamental result of multivariate calculus, in Isabelle/HOL. The theorem statement that we formalise is enough for most applications, especially in physics and engineering. An interesting aspect of our proof is that we neither formalise orientations nor region boundaries explicitly, with respect to the outwards-pointing normal vector. Instead we refer to homological equivalences between paths.

The slides of the talk can be found in the following link.

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.

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.