Proyecto ECOS U00E02 de colaboración Uruguay-Francia

Especificaciones y Programas: Modelos de Cálculo, Tipos e Implementaciones

Instituciones

Investigadores

Resumen de la Investigación

El plan consiste en la definición y la investigación de las propiedades de ciertos cálculos tipados (inspirados del cálculo lambda), que permiten la modelización de la especificación de un problema y del programa que lo resuelve. Nos interesa estudiar propiedades como por ejemplo la confluencia y la normalización: la primera asegura el determinismo del sistema, y la segunda la existencia de un resultado para cada computación.
Los sistemas de tipos, y los algoritmos de inferencia de tipos, son importantes en este marco ya que permiten, en muchos casos, la verificación automática de estas propiedades, además de proteger las estructuras de datos y los operadores contra usos incorrectos. Por ejemplo, en el cálculo lambda, los subsistemas tipados son fuertemente normalizantes (todas las computaciones terminan). Este resultado es válido en sistemas de tipos muy diferentes, que van de los tipos simples al Cálculo de Construcciones. Entre las posibles extensiones de los cálculos que nos proponemos estudiar, está la inclusión de tipos inductivos, y de reglas de reducción arbitrarias sobre éstos (utilizando sistemas de reescritura de términos).
Si bien en los sistemas tipados todas las computaciones permiten obtener el resultado deseado, es importante definir una estrategia que llegue a este resultado lo más rápido posible. Desde un punto de vista práctico, para obtener una implementación eficiente de estos cálculos, nos proponemos estudiar diferentes estrategias de computación y comparar sus performances. La herramienta que nos servirá de base en este estudio es la Lógica Lineal y sus derivados, como las redes de interacción, que inspiraron la definición de estrategias eficientes (y optimales) en el cálculo lambda gracias a la descomposición en acciones atómicas de cada paso en la computación.
En la Teoría de Especificaciones se presenta una teoría formal de la programación basada en la Teoría Constructiva de Tipos, obteniendose una noción de programa más realista que la que existe en las distintas formulaciones de la teoría de tipos pero manteniendo las ventajas que tiene la utilización de dichas teorías, esto es: la unificación de conceptos, el hecho que la verificación de programas se reduce a un control de tipos, y la posibilidad de construir en paralelo los programas y sus pruebas de corrección.
En este proyecto proponemos iniciar el proceso de construcción de un asistente que permita utilizar en la practica la teoría de Especificaciones. Para ello, las principales etapas son: el estudio de las relaciones entre tipos y normalización, el desarrollo de un algoritmo de control de tipos, y el estudio de estrategias eficientes de reducción utilizando técnicas derivadas de la Lógica Lineal.

Presentación del Proyecto

Documentación

  • Artículos publicados
  • Informe 2000-2002 (documento postcript)