Noticias
“Equivalences for Free: Univalent Parametricity for Effective Transport” is the title of work of Éric Tanter, professor at the Department of Computer Science of the University of Chile and associate researcher of the Millennium Institute for Foundational Research on Data, which -carried out in conjunction with the researchers Nicolas Tabareau and Matthieu Sozeau, of the French National Institute for Computer Science and Applied Mathematics (Inria)-, received the Distinguished Paper Award, at the 23rd ACM SIGPLAN International Conference on Functional Programming (ICFP 2018).
The conference, which took place in the United States, is one of the most prestigious in the area of programming languages: “This recognition is a great honor and it gives an important visibility to our research. According to the conference committee, it is an article that, due to its novelty and potential long-term impact, everyone should read”, said professor Éric Tanter.
Tanter highlighted that the research represents a contribution in the area of certified programming and test assistants, such as Coq and Agda. “Our paper demonstrates that in Coq’s theory of types, it is possible to carry out to a large extent the principle of univalence” of the theory of homotopic types in a constructive way. Univalence is a principle that allows to handle equivalences (semantic) as equalities (syntactic), facilitating formal reasoning. Until now, it was not known how to integrate this principle into practice”, explains the IMFD researcher.
Éric Tanter added that the award is a recognition to his research on more fundamental topics in the area of programming languages, which began around 2010. “For the Departamentof Computer Science of the University of Chile, as also for the Millennium Institute for Foundational Research on Data (IMFD), this high-level recognition on the international scenario affirms the relevance of the cutting edge research we are doing”, Tanter stated.
Professor Tanter also pointed out that the work is the result of an international collaboration project Conicyt Redes CSEC (Certified Software Engineering in Coq), funded for 2018-2019, and an Equipe Associée Inria.
Source: Communications DCC U. de Chile
