¿Qué puede hacer la investigación en informática para ayudar a la dislexia?

 

Ponente: Luz Rello Sánchez (Carnegie Mellon University, sitio web)

Lugar: Salón de Actos (Edificio CCT)

Hora: lunes 22 de enero, 11:00

Resumen: En esta intervención Luz Rello hará un resumen de los últimos siete años de investigación multidisciplinar desarrollada entre la Universidad Pompeu Fabra, Carnegie Mellon University y Change Dyslexia para llegar hasta la presentación de las aplicaciones de detección precoz de dislexia y de apoyo a la dislexia: Dytective Test y DytectiveU, validadas con 10.000 personas. Ambas herramientas mezclan técnicas de aprendizaje automático, procesamiento del lenguaje natural así como técnicas de evaluación de interacción hombre-máquina.

Breve reseña biográfica: Luz Rello es una investigadora española que empezó su trayectoria en el ámbito de la Lingüística en la Universidad Complutense de Madrid. Posteriormente realizó estudios en Procesamiento de Lenguaje Natural. En estos momentos se encuentra realizando su Tesis Doctoral en la Carnegie Mellon University (Pittsburgh, Estados Unidos) y ha sido acreedora de diversos premios nacionales e internacionales entre los que se encuentran el Premio a la Excelencia Académica de la Comunidad de Madrid 2007 – 2008, la Beca Google Anita Borg 2011 o la Beca Santander para Jóvenes Profesores e Investigadores 2012. En 2013, Rello Sánchez fue galardonada con el European Young Researchers’ Award (EYRA), el cual otorga la organización Euroscience, ​ por su trabajo de investigación en el área de ciencias de la computación y accesibilidad para personas con dislexia (ha sido la primera investigadora española en obtener este galardón).

Una breve introducción a la Programación Orientada a Aspectos

Ponente: Beatriz Pérez Valle (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 17 de enero, 11:00

Resumen: Durante el desarrollo de aplicaciones, suelen aparecer problemas que los desarrolladores no pueden resolver de una manera adecuada con las técnicas habituales usadas en paradigmas de programación como POO o PP. Este es el caso de la implementación de determinados aspectos que refieren a requisitos transversales compartidos por todos o por parte de las componentes base de la aplicación y que no pueden encapsularse dentro de una única unidad funcional (ej. monitorización, manejo de errores, seguridad…). Como consecuencia, los desarrolladores se ven forzados a tomar decisiones de diseño que repercuten de manera importante en el desarrollo de las aplicaciones, obteniendo como resultado código redundante, difícil de modificar y mantener.

La programación orientada a aspectos (aspect-oriented programming o AOP) es un nuevo paradigma de programación cuyo principal objetivo es la modularización de las aplicaciones, fomentando una mejor separación de los elementos que son transversales a todo el sistema.

El seminario pretender dar una breve introducción a la programación orientada a aspectos centrándose, como caso particular, en AspectJ como extensión de Java para la AOP.

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

 

Diagramas UML como herramienta para el diseño de provenance

 

Ponente: Carlos Sáenz Adán (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: miércoles 20 de diciembre, 11:00

Resumen: El provenance es considerado como información sobre entidades, actividades y personas involucradas en la producción/manipulación de información. En particular, a través del provenance se puede ofrecer información esencial a la hora de verificar la calidad y fiabilidad de los resultados obtenidos tras la ejecución de un programa. De hecho, la “United States Association for Computational Mechanics” ha identificado recientemente el provenance como uno de los principios que garantizan la transparencia y fiabilidad de los datos.

En la charla se abordará el provenance desde el punto de vista de la Ingeniería del Software, comenzando con una breve introducción a provenance y en particular, a su estándar W3C PROV y el desarrollo PROV-Templates. A continuación, se profundizará en la generación automática de PROV-Templates a partir de Diagramas UML. Concretamente, se mostrará la generación de PROV-Templates a partir de Diagramas de Clases UML, y la adaptación de una propuesta anterior en la transformación de Diagramas de Secuencia UML. Posteriormente veremos cómo es posible la utilización de la Programación Orientada a Aspectos para la captura de información durante la ejecución de un programa. Y finalmente, terminaremos con un caso de uso que ilustra el trabajo realizado.

Nota: Las contribuciones presentadas en esta charla han sido desarrolladas en una estancia de investigación en el King’s College London junto al profesor Luc Moreau y Simon Miles, reconocidos autores en el campo del provenance.

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

Documentos electrónicos accesibles: donde existe una necesidad, nace un derecho

 

Ponente: Eduardo Sáenz de Cabezón Irigaray (Universidad de La Rioja)

Lugar: Seminario Mirian Andrés (Edificio CCT)

Hora: lunes 27 de noviembre, 12:00

Resumen: La accesibilidad web y en documentos electrónicos es de imprescindible importancia para un cierto porcentaje de la población, importante para un porcentaje más amplio y conveniente para todos.

En esta charla abordaremos los principios fundamentales de la accesibilidad en el contexto del acceso a la información y daremos algunas recomendaciones sencillas para que nuestros documentos se acerquen a ser universalmente accesibles.

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

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.