GRAPA: Asistentes de prueba gradual

Resumen del proyecto:

El objetivo principal de este equipo de investigación franco-chileno es extender el alcance de la tipificación gradual a teorías de tipos completas para respaldar la programación certificada fluida en una nueva generación de asistentes de prueba.

Los objetivos son:

• Razonamiento Interno sobre Precisión y Gradualidad: en este proyecto, se seguirá desarrollando las ideas iniciales de internalizar la precisión y la gradualidad, basándonos en trabajos recientes sobre igualdad observacional y extendiéndose a otras variantes graduales de CIC (por ejemplo, con gradualidad global) para demostrar sus beneficios. En particular, se extenderán los resultados iniciales en un cálculo de molde (GRIP) a un lenguaje de origen similar a GCIC y se estudiarán la integración de tipos inductivos indexados generales en esta configuración.

• Implementaciones de la teoría del tipo gradual: Hasta la fecha, todos los avances en los tipos dependientes graduales y la teoría de tipos graduales han sido esencialmente teóricos: no hay implementación de GDTL o GCIC. El objetivo del equipo es abordar esta brecha, hacia implementaciones utilizables de teorías de tipo gradual para una nueva generación de pruebas asistentes.

En Francia:

• Nicolas Tabareau, investigador, coordinador del proyecto GRAPA, equipo-proyecto GALLINETTE, Centro Inria de la Université de Rennes, Inria

• Kenji Maillard, investigador, equipo-proyecto GALLINETTE, Centro Inria de la Université de Rennes, Inria

• Koen Jacobs, investigador postdoctoral, equipo-proyecto GALLINETTE, Centro Inria de la Université de Rennes, Inria

En Chile:

• Éric Tanter, investigador, coordinador del proyecto GRAPA, Universidad de Chile

• Stefan Malewski, estudiante de doctorado, Universidad de Chile

• Tomas Diaz, estudiante de doctorado, Universidad de Chile

• https://inria.cl/es/grapa-asistentes-de-prueba-mas-accesibles