Noticias
«Equivalences for Free: Univalent Parametricity for Effective Transport” se titula el trabajo de Éric Tanter, académico del Departamento de Ciencia de la Computación de la Universidad de Chile e investigador asociado del Instituto Milenio Fundamentos de los Datos, que -realizado en conjunto con los investigadores Nicolas Tabareau y Matthieu Sozeau, del French National Institute for Computer Science and Applied Mathematics (Inria)-, fue reconocido como Distinguished Paper Award, en la 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP 2018).
La conferencia, que tuvo lugar en Estados Unidos es una de las más prestigiosas en el área de lenguajes de programación: “Recibir este reconocimiento es un tremendo honor, además de la visibilidad que le da a nuestra a investigación. Según el comité de la conferencia es un artículo que por su novedad y potencial impacto a largo plazo todos deberían leer”, señaló el profesor del DCC Éric Tanter.
El académico del DCC de la U. de Chile destacó que la investigación representa una contribución en el área de programación certificada y asistentes de pruebas, como Coq y Agda. “Nuestro paper demuestra que en la teoría de tipos de Coq, es posible realizar en gran medida el principio de “univalencia” de la teoría de tipos homotópicos de manera constructiva. La univalencia es un principio que permite manejar equivalencias (semánticas) como igualdades (sintácticas), facilitando el razonamiento formal. Hasta ahora, no se sabía cómo integrar este principio en la práctica”, explica el investigador del IMFD.
El profesor Éric Tanter agregó a su vez que el premio valida su reconversión científica hacia temáticas más fundamentales en el área de los lenguajes de programación, iniciada alrededor del 2010. “Para el DCC, en tanto, este reconocimiento de alto nivel en el escenario internacional es una forma de afirmar su relevancia en investigación de punta. Somos muchos los que hemos brindado dichos reconocimientos al departamento, y siempre es un orgullo contribuir así a su prestigio. En el DCC se hace investigación de calidad”, destacó.
Para finalizar, el académico señaló que el trabajo es fruto del proyecto de colaboración internacional Conicyt Redes CSEC (Certified Software Engineering in Coq), financiado para 2018-2019, y un Equipe Associée Inria.
Fuente: Comunicaciones DCC U. de Chile
