GRAPA - Gradual Proof Assistants

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.

• Nicolas Tabareau, investigador, coordinador del proyecto GRAPA, equipo-proyecto GALLINETTE, Inria
• Kenji Maillard, investigador, equipo-proyecto GALLINETTE, Inria
• Koen Jacobs, Postdoc, Inria Chile y equipo-proyecto GALLINETTE, Inria
• É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