GRAPA: asistentes de prueba más accesibles

En este Equipo Asociado colaboran investigadores del centro Inria de la Université de Rennes y de la Universidad de Chile. Esta vez, hablamos con sus coordinadores, Nicolas Tabareau, investigador líder del equipo-proyecto Gallinette, y Éric Tanter, profesor del del Departamento de Ciencias de la Computación de la Facultad de Ciencias Físicas y Matemáticas de la  Universidad de Chile e investigador del grupo Pleiad, para conocer más acerca de su trabajo colaborativo. 

Los lenguajes dinámicos son flexibles y de fácil acceso, pero no ofrecen ninguna garantía de corrección por construcción. El equipo asociado GRAPA está interesado en la posibilidad general de combinar enfoques estáticos y dinámicos dentro del entorno desafiante de las teorías de tipos dependientes, apoyando así la programación certificada gradual. 

Un enfoque gradual permite a los programadores disfrutar de los beneficios del razonamiento estático y conservador en la medida que lo deseen, aplazando el análisis restante al tiempo de ejecución. El objetivo principal del equipo de GRAPA es, por lo tanto, extender el alcance de la tipificación gradual a teorías de tipos completas para respaldar la programación certificada sin problemas en una nueva generación de asistentes de prueba.

ET: Nuestros equipos de investigación han estado colaborando durante más de 10 años. Hemos tenido equipos asociados continuamente desde entonces. Esto es en sí mismo un seguimiento de mi tesis doctoral que fue codirigida con la Université de Nantes en 2000-2004, y mi colaboración con Nantes hasta que Nicolas Tabareau se unió a Inria en 2009.

NT: Cuando me uní a Inria en 2009, Éric Tanter ya estaba colaborando activamente con investigadores en Nantes sobre otros temas. Rápidamente logramos fusionar nuestros diferentes antecedentes para atacar un nuevo problema, en la frontera de los asistentes de prueba y los lenguajes de programación convencionales.

Crédito

© Inria / Photo M. Magnin

ET: Mi laboratorio, Pleiad, está estudiando varios lenguajes de programación e ingeniería de software, con un enfoque reciente en sistemas de tipos, verificación de programas y semántica. El equipo Gallinette de Inria, dirigido por Nicolas Tabareau, se centra en el avance de la Teoría de Tipos en general y el asistente de prueba Coq en particular.

NT: Al utilizar la competencia del equipo Pleiad y Gallinette, nos gustaría ver cómo se pueden reutilizar las técnicas para obtener lenguajes de programación convencionales más flexibles en el entorno de los asistentes de prueba basados en la teoría de tipos, que son lenguajes de programación muy peculiares, pero aun así lenguajes de programación

ET: Además de las contribuciones teóricas, esperamos:

• producir una implementación práctica de un asistente de prueba gradual, probablemente como una extensión del asistente de prueba Coq;
• llegar a una implementación a nivel de producción es probablemente demasiado ambicioso en este punto, pero al menos podemos avanzar en una prueba de concepto utilizable, aplicable a proyectos de tamaño pequeño a mediano.

ET: He estado trabajando en escritura gradual en lenguajes de programación durante más de una década, y Tabareau es un experto en teoría de tipos y asistentes de prueba. Por lo tanto, el proyecto GRAPA realmente explota esta sinergia entre ambas líneas de experiencia.