Presentación Grupo ELP |
El grupo ELP (Extensiones de la Programación Lógica) está formado por los siguientes componentes. Las principales tareas de investigación están encaminadas al estudio, desarrollo y optimización de los lenguajes declarativos.
Aquí puedes encontrar una pequeña introducción sobre nuestro campo de investigación. Las principales áreas en las que estamos trabajando actualmente son las siguientes:
Modelización funcional de procesos concurrentesEl sistema formal de partida es el lambda cálculo etiquetado paralelo (LCEP). Trabajamos en la mecanización de la ejecución de procesos mediante la utilización de técnicas de reescritura, con el objetivo de construir un intérprete para el lenguaje basado en las técnicas desarrolladas. Asimismo, investigamos el problema de establecer una interpretación semántica empleando para ello un enfoque algebraico, extendiendo el cálculo para trabajar con tipos y desarrollando un compilador para un lenguaje de más alto nivel orientado a objetos que utilice los recursos de la máquina abstracta de forma eficiente.
Extensiones de los lenguajes lógicos: negaciónLos estudios realizados para el desarrollo de un método constructivo sugieren el interés de considerar otros tipos de negación por defecto (fallo finito, negación en teorías disyuntivas, etc). Consideramos la formalización de estos modelos, tanto para el caso lógico (teorías disyuntivas) como para el caso lógico-funcional. En particular, estudiamos la propiedad de composicionalidad tanto de la negación constructiva como del fallo finito para programas lógicos y lógico-funcionales.
Extensiones de los lenguajes funcionales: orden superior y programación con restricciones de reemplazamientoOtra extensión consiste en que al ejecutar programas funcionales de primer orden, a menudo surge el problema de limitar los pasos de ejecución permitidos, con el fin de obtener un mejor comportamiento operacional: mejorar la terminación del programa o evitar realizar pasos innecesarios. En el apartado de programación con restricciones de reemplazamiento estudiamos cómo limitar las computaciones funcionales de forma que: no se altere el resultado obtenido cuando la computación se lleva a cabo de forma libre, se mejore el comportamiento operacional del programa en los sentidos antes mencionados y se puedan especificar las restricciones de reemplazamiento de forma automática, es decir, sin que sea necesaria la intervención del programador.
Análisis semántico y transformación de programas lógico-funcionalesEn el apartado de análisis semántico de programas, trabajamos en el desarrollo de un marco general de aproximación de programas lógico-funcionales que permita caracterizar diferentes aspectos de su ejecución. La composicionalidad de la semántica concreta y de su contrapartida abstracta resultan esenciales para conseguir análisis precisos y eficientes.
En el apartado de transformación de programas, trabajamos en el desarrollo de técnicas eficientes de desplegado y evaluación parcial de programas que preserven la semántica a lo largo del proceso de transformación. Estas técnicas se utilizarán para optimizar la ejecución del programa (y su versión abstracta) sin pérdida de corrección.