Sistemas de Tipos Dependientes
Los sistemas de tipos dependientes presentan el concepto de familia de tipos o tipo parametrizado por objetos de otros tipos. Ellos hacen posible la expresión de estructuras refinadas de datos, haciendo explícitos invariantes complejos de las mismas.
Como consecuencia, el control de tipos permite garantizar propiedades fuertes de las construcciones realizadas, por ejemplo, corrección total de programas respecto a especificaciones funcionales completas expresadas como tipos, o ajuste de derivaciones respecto a reglas de sistemas formales.
Trabajamos en:
- Programación con Tipos Dependientes, con el objetivo de mediano plazo de completar un tratado sistemático. En este plano son importantes:
- El estudio sistemático de técnicas de diseño de estructuras de datos que alivien la carga de matemática explícita asociada en estos lenguajes a la programación certificada.
- El estudio del diseño de lenguajes mínimos y sistemas de programación confiables en los que efectuar estos desarrollos.
- El desarrollo de los métodos de análisis cuantitativo de estructuras de datos y algoritmos.
- Metateoría e infraestructura formales, es decir, la Matemática formal de los lenguajes de programación y sus implementaciones, así como de los sistemas formales de Lógica. En este plano trabajamos actualmente en:
- Metateoría del Cálculo Lambda en Teoría Constructiva de Tipos.
- Comparación de técnicas de tratamiento de las variables ligadas y la sustitución.
- Control de Tipos certificado.
- Estructuras de Lógicas que representen una abstracción del concepto de sistema formal y el desarrollo de asistentes de demostración generalizados. Actualmente trabajamos en: sistemas de tipos dependientes para la Sintaxis Abstracta Nominal, con el fin de proveer una estructura de lógicas más básica y simple que las basadas en el Cálculo Lambda.
Generación automática de código paralelo
Hasta hace poco, las mejoras en performance de los procesadores, obtenidas esencialmente por el aumento de la frecuencia, de la cantidad de transistores y del flujo de instrucciones por ciclo, impactaban de manera prácticamente directa en la del software.
Esto permitía paliar las teóricas deficiencias en performance del software secuencial recurriendo a sofisticadas, pero efectivas, técnicas de compilación.
Esto está cambiando rápidamente debido a barreras que limitan la progresión de la performance del hardware: la imposibilidad de seguir aumentando la frecuencia, el aumento de la probabilidad de error debajo de los 65nm y la lentitud relativa de la memoria.
Por esto, la industria del hardware está desarrollando arquitecturas con múltiples procesadores. Ahora, la explotación de la performance ya no pasa por una compilación inteligente del software secuencial, sino por el diseño de software explícitamente concurrente.
Este cambio, aunque en principio tecnológico, trajo consigo un conjunto de problemas de carácter científico que necesitan ser estudiados en profundidad. Desde el punto de vista del desarrollo de software, estos problemas están ligados, en particular, aunque no de manera excluyente, a la proliferación de paradigmas, arquitecturas y modelos de programación concurrente.
El objetivo de este proyecto es investigar técnicas rigurosas de diseño, implementación y análisis para desarrollar software paralelo, teniendo en cuenta propiedades de corrección, performance y productividad.
En particular, se busca validar la tesis que la generación automática de código a partir de especificaciones formales de alto nivel mediante el uso de transformaciones formales es una buena herramienta para resolver los problemas mencionados.