Introducción al formalismo de las Gramáticas de Atributos, características y clasificación. Métodos de evaluación. Aplicaciones para el cómputo sobre árboles con atributos (generación de procesadores de lenguajes). Relaciones con los paradigmas de programación funcional y lógica. Herramientas existentes.
Presentación

Una propuesta para apoyar la enseñanza de métodos formales en una currícula de grado, usando el asistente de pruebas Coq y conceptos del área de Teoría de Tipos. Se propone un taller de especificación, derivación y verificación de sistemas en los paradigmas de programación funcional e imperativo, que puede también ser adaptado a sistemas reactivos y de tiempo real. Se describen experiencias en el desarrollo del taller y se plantean posibles cambios y extensiones.
Presentación

Para el análisis de sistemas de tiempo real se destacan dos enfoques formales: la verificación de modelos y el análisis deductivo basado en asistentes de prueba. El primero se caracteriza por ser completamente automatizable pero presenta dificultades al tratar sistemas con un gran número de estados o que tienen parámetros no acotados. El segundo permite tratar con sistemas arbitrarios pero requiere la interacción del usuario. Este trabajo explora una metodología que permite compatibilizar el uso de un verificador de modelos como Kronos y el asistente de pruebas Coq en el análisis de sistemas de tiempo real. Se pone especial énfasis en el análisis de un caso de estudio, considerado como un benchmark en diferentes trabajos: el control de un paso a nivel de tren.
Presentación

En esta charla se describirá una técnica de producción automática de programas conocida como Especialización de Tipos, y se explicarán los últimos resultados obtenidos en el área, como parte de la tesis de doctorado del disertante.
Presentación

Los lenguajes funcionales poseen un alto nivel de abstracción que contribuye al proceso de diseño y construcción de software. El programador funcional suele no preocuparse por aspectos de bajo nivel, tales como uso y gerenciamiento de memoria. Estos aspectos, así como la generación de código eficiente, pasan a ser en gran medida responsabilidad del compilador, por lo que toda optimización de código que el compilador pueda realizar pasa a ser de particular relevancia. Existe una gran variedad de técnicas de transformación de programas cuyo objetivo es optimizar código. Una de dichas técnicas se conoce como fusión. Su utilización en la optimización de programas funcionales se origina en el uso frecuente y sistemático de la operación de composición de funciones como forma de estructurar los programas. Los programas así escritos suelen ser más legibiles y su mantenimiento más sencillo, pero a la vez menos eficientes debido a que toda composición tiene asociada la construcción y consumo de una estructura de datos intermedia. La técnica de fusión tiene como objetivo la eliminación automática de tales estructuras intermedias. Se basa en ciertas leyes algebraicas entre programas, conocidas como leyes de fusión, que suelen estar asociadas a un conjunto de operadores recursivos (e.g. fold, map, etc.), que encapsulan patrones comunes de computación y dan origen a un mecanismo adicional de estructurar los programas. En esta charla presentaremos los aspectos principales de una herramienta, llamada HFusion, que permite la fusión automática de programas escritos en Haskell.
Presentación