Proyecto ECOS U00E02 de colaboración Uruguay-Francia
Especificaciones y Programas: Modelos de Cálculo,
Tipos e Implementaciones
Instituciones
-
Instituto de Computación - Facultad de Ingeniería - Universidad
de la República (In.Co.)
-
Laboratoire d' Informatique (CNRS UMR 8548) - Ecole Normale Superieure,
Paris.
Investigadores
-
Uruguay
-
Nora Szasz, Profesor Asociado, InCo, Facultad de Ingeniería
-
Paula Severi, Profesor Adjunto, Instituto de Matemática, facultad
de Ciencias
-
Francia
-
Giuseppe Longo, Laboratoire d?Informatique, École Normale Supérieure,
Paris
-
Maribel Fernández, Maître de Conférences, Laboratoire
d'Informatique (LIENS - UMR 8548)
-
Ian Mackie, Chargé de Recherche, CNRS - Chef de Travaux Pratiques,
École Polytechnique - LIX (CNRS UMR 7650)
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
El resumen del area de investigación, antecedentes del equipo
de investigación, los objetivos del proyecto y la metodología
de trabajo son detallados en el
documento de propuesta.
Documentación
-
Artículos publicados
-
Informe 2000-2002 (documento
postcript)