Éric Tanter receives Inria International Chair

Éric Tanter, professor in the Department of Computer Science at the University of Chile and associate researcher at Millennium Institute Foundational Research on Data, was awarded an Inria International Chair, a program that promotes collaboration between leading international researchers and the French research center, one of the world's leading science and technology research centers.

"These international chairs are highly prestigious and very competitive," says Tanter. "They represent anopportunity to delve deeper into research topics that are not only relevant on a global level, but also strengthen Chile's presence in the international scientific community. It is recognition of the quality of the work we do in Chile, in collaboration with colleagues from around the world."

The Inria International Chairs consist of recruiting experienced international researchers for periods of 10 or 12 months, spread over five years (in this case, 2025-2029). These chairs are highly competitive: the evaluation is based primarily on the researcher's track record, as well as on the associated research proposal. This recognition reflects Tanter's excellent work and his contribution to high-level research in the field of programming languages and logic.

The investigation

Éric Tanter will develop a research agenda on Malleable Proof Assistants, reinforcing a long-standing collaboration with Inria's Gallinette team on the GRAPA (Gradual Proof Assistants) project .

This line of research focuses on the need to correct software systems, which have become central to society, making it essential to ensure they function correctly. One of the most robust and promising approaches to guaranteeing this functioning is verification carried out in testing assistants such as Rocq and Lean, known as certified programming. This approach has been certified for its advantages in large-scale projects, such as the CompCert certified C compiler .

"The certified programming projects that have been successful to date remain impressive development efforts, requiring the work of many PhD-level experts over several years. The rigidity and complexity of test assistants make these technologies difficult to access for beginners and non-specialist engineers, "the researcher notes.

This project seeks to ease this barrier by promoting the malleability of test assistants through three complementary axes: incrementality, graduality, and extensibility. "For each axis, we aim to contribute to both the foundational and practical aspects, developing theoretical foundations as well as prototyping mechanisms and tools for the Rocq provider."

"The Gallinette team is in charge of developing and evolving the Rocq testing assistant, and is very active in the area of type theory, the formalism underlying these tools. In addition, the idea is also to collaborate with other Inria teams working on type theory and testing assistants, mainly in Paris and Rennes, as well as Nantes," explains the academic.

The potential of the work carried out in Chile and international collaboration

For the researcher, this is an "example of the potential of the top-level research carried out in Chile, hosted by the University of Chile and an internationally renowned institute such as the Millennium Institute Foundational Research on Data."

He also emphasizes that this is the result of long-standing international collaboration: "High-quality research is rarely the work of a lone genius; rather, it is the product of interactions and mutual enrichment with other People In this case, it is the result of a thematic shift that began about 10 years ago and could not have been achieved without the synergy with several People, especially Nicolas Tabareau, the researcher responsible for Gallinette at Inria, who was already an expert in these topics when I first became interested in them."

"I am convinced that high-quality research can and should be carried out in Chile, and that these types of distinctions inspire new generations of scientists in our country," says the academic.