Éric Tanter recibe Cátedra Internacional de Inria
Éric Tanter, académico del Departamento de Ciencias de la Computación de la Universidad de Chile e investigador asociado del Instituto Milenio Fundamentos de los Datos, recibió una Cátedra Internacional de Inria (Inria International Chair), programa que fomenta la colaboración de destacados investigadores internacionales y el centro de investigación francés, uno de los principales centros de investigación de ciencia y tecnología a nivel mundial.
«Estas cátedras internacionales son de alto prestigio y muy competitivas», comenta Tanter. «Representan una oportunidad para profundizar en temas de investigación que no sólo son relevantes a nivel global, sino que también fortalecen la presencia de Chile en la comunidad científica internacional. Es un reconocimiento a la calidad del trabajo que realizamos desde Chile, en colaboración con colegas de todo el mundo.»
Las Inria International Chairs consisten en el reclutamiento de experimentados investigadores internacionales por periodos de 10 o 12 meses, distribuidos en cinco años (en este caso, 2025-2029). Estas cátedras son muy competitivas: la evaluación se basa principalmente en la trayectoria del investigador, como también en la propuesta de investigación asociada. Este reconocimiento refleja el trabajo de excelencia de Tanter y su contribución a la investigación de alto nivel en el campo de los lenguajes de programación y la lógica.
La investigación
Éric Tanter desarrollará una agenda de investigación sobre Asistentes de Demostración Maleables (Malleable Proof Assistants), que llega a reforzar una colaboración de larga data con el equipo Gallinette de Inria en el proyecto GRAPA – Gradual Proof Assistants.
Esta línea de investigación se enfoca en la necesidad de corrección de los sistemas de software, los que se han hecho centrales en la sociedad, por lo que garantizar su correcto funcionamiento es clave. Uno de los enfoques más sólidos y prometedores para garantizar este funcionamiento es la verificación que se lleva a cabo en asistentes de prueba como Rocq y Lean, conocida como programación certificada. Esta aproximación cuenta con certificación de sus ventajas en proyectos de gran escala, como el compilador de C certificado CompCert.
“Los proyectos de programación certificada que han tenido éxito hasta la fecha siguen siendo esfuerzos de desarrollo impresionantes, que requieren el trabajo de muchos expertos de nivel de doctorado durante varios años. La rigidez y complejidad de los asistentes de pruebas hacen difícil el acceso a estas tecnologías a principiantes e ingenieros no especializados”, señala el investigador.
Este proyecto busca suavizar esta barrera, fomentando la maleabilidad de los asistentes de pruebas a través de tres ejes complementarios: incrementalidad, gradualidad y extensibilidad. “Para cada eje, pretendemos contribuir tanto en los aspectos fundacionales como en los prácticos, desarrollando fundamentos teóricos así como mecanismos y herramientas de prototipado para el prover Rocq”
“El equipo Gallinette está a cargo del desarrollo y la evolución del asistente de pruebas Rocq, y muy activo en el área de teoría de tipos, el formalismo subyacente a estas herramientas. Además, la idea es también colaborar con otros equipos de Inria que trabajan en teoría de tipos y asistentes de pruebas, principalmente en París y Rennes, además de Nantes”, explica el académico.
El potencial del trabajo realizado en Chile y la colaboración internacional
Para el investigador, este es un “ejemplo del potencial de la investigación de primer nivel que se realiza en Chile, alojada en la Universidad de Chile y un instituto de relevancia internacional cómo lo es el Instituto Milenio Fundamentos de los Datos”.
Además, destaca que que esto es el fruto de una larga colaboración internacional: “La investigación de calidad es raramente el fruto de un genio aislado, es más bien producto de interacciones y enriquecimiento mutuo con otras personas. En este caso, es el resultado de un cambio temático que inicie hace unos 10 años y que no podría haber logrado sin la sinergia con varias personas, especialmente Nicolas Tabareau, el investigador responsable de Gallinette en Inria, que ya era experto en estos temas cuando yo empecé a interesarme en ellos”.
«Estoy convencido de que la investigación de calidad puede y debe desarrollarse desde Chile, y que este tipo de distinciones inspiran a las nuevas generaciones de científicos en nuestro país», señala el académico.