Noticias

Investigador Éric Tanter publica investigación en Journal of the ACM

“The Marriage of Univalence and Parametricity”, se titula el artículo del investigador del Instituto Milenio Fundamentos de los Datos y profesor del Departamento de Ciencias de la Computación (DCC) Éric Tanter, junto a los investigadores de Inria Nicolas Tabareau y Matthieu Sozeau, el cual fue publicado en la Journal of the ACM (JACM), que es la revista más prestigiosa en computación y de alcance máximo.

El profesor del DCC explicó que los asistentes a la demostración (“proof assistants”) como Coq, Agda o Lean, permiten escribir enunciados matemáticos y llevar a cabo su demostración formal, usando la máquina como mecanismo de verificación automático que asegura que la demostración formal es efectivamente correcta. “Hoy día, los proof assistants tienen dos áreas principales de aplicación: para mecanización de resultados matemáticos de cualquier índole, y para esfuerzos de verificación de programas”, explicó Éric Tanter.

A su vez, el profesor destacó que estos asistentes son lenguajes de programación basados en teorías de tipos dependientes, y por ende tienen un doble rol como herramientas para desarrollar programas y desarrollar demostraciones. “Una piedra de tope fundamental en el uso de estas teorías es que la noción de igualdad (es decir, ¿qué significa que dos términos—expresiones, funciones, tipos, etc.—sean iguales?) es esencialmente sintáctica, y no semántica. En cambio, los humanos, y los matemáticos, estamos acostumbrados a explotar nociones de equivalencias (como isomorfismos) para razonar, y construir nuestras demostraciones”, destacó el profesor.

El trabajo realizado consiste en analizar de cerca dos nociones potentes para explotar equivalencias en demostraciones y programas, que son la parametricidad (del informático John Reynolds) y la más reciente noción de univalencia (del matemático Vladimir Voevodsky). “El artículo destila los pros y cons de cada una, y propone una nueva noción, la “parametricidad univalente”, la cual permite programar y demostrar modulo equivalencias”, señaló Éric Tanter.

Esta investigación además de proponer esta nueva noción de parametricidad univalente, describe toda la meta-teoría asociada. “El trabajo tiene un componente práctico importante, ya que presentamos una implementación de una librería para extender Coq con dicha noción, y proveemos múltiples ejemplos de razonamiento e implementación modulo equivalencias”, comentó el profesor.

Cabe destacar que una versión previa de este trabajo fue previamente premiada con un “Distinguished Paper Award”, en la conferencia ICFP del ACM el año 2018. “En base al alto interés y valiosa retroalimentación que obtuvimos en ese entonces, seguimos trabajando en simplificar la presentación formal de la parametricidad univalente, a la vez mejoramos el aspecto práctico de la realización en Coq y decidimos mandar el trabajo mejorado a la revista Journal of the ACM (JACM), la cual es simplemente la revista más prestigiosa en computación de alcance máximo, y de larguísima historia”, enfatizó Éric Tanter.

«El Journal of the ACM es uno de los espacios más relevantes a nivel internacional para el estudio de ciencia de computación, por lo que esta publicación destaca en su área, posicionando a la investigación como una de las más avanzadas de su categoría», señala Marcelo Arenas, director del IMFD.

The Journal of the ACM (JACM) provides coverage of the most significant work on principles of computer science, broadly construed. The scope of research covered encompasses contributions of lasting value to any area of computer science. To be accepted, a paper must be judged to be truly outstanding in its field. JACM is interested in work in core computer science and in work at the boundaries, both the boundaries of subdisciplines of computer science and the boundaries between computer science and other fields.

Para finalizar, el profesor destacó que esta publicación más allá del prestigio de la revista, es uno de los trabajos más significativos en su carrera académica. “Es fruto de una larga e intensa colaboración de más de 10 años con mi colega y amigo Nicolas Tabareau de Inria en Francia. Abarca una temática que me fascina desde que la descubrí durante una estadía de investigación en EEUU en 2009: la correspondencia de Curry-Howard entre lógicas formales y lenguajes de programación, de la cual la teoría de tipos dependientes es el ejemplar más poderoso. Si bien el tema estaba muy alejado de mi especialidad cuando me lo enseñaron, quedé totalmente fascinado y decidí orientar parte de mis esfuerzos en esa dirección. Con la ayuda de Nicolas y otros colaboradores expertos en el área como Matthieu Sozeau, he podido desempeñarme en esta colaboración, aprender muchísimo, y hoy ser parte de una contribución sólida”, concluyó.