Éric Tanter receives Inria International Chair

Éric Tanter, academic at the Departamento de Ciencias de la Computación de la Universidad de Chile and associate researcher at the Millennium Institute for Foundational Research on Data (IMFD), received an Inria International Chair, a program that fosters collaboration between prominent international researchers and the French research center, one of the leading science and technology research centers in the world.

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

The Inria International Chairs involve 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 outstanding work and his contribution to high-level research in the field of programming languages and logic.

The Research

Éric Tanter will develop a research agenda on Malleable Proof Assistants, which reinforces a long-standing collaboration with the Gallinette team at Inria on the GRAPA – Gradual Proof Assistants project.

This research line focuses on the need for correctness in software systems, which have become central to society, making it essential to guarantee their proper functioning. One of the most solid and promising approaches to guaranteeing this functioning is verification carried out in proof assistants such as Rocq and Lean, known as certified programming. This approach has demonstrated its advantages in large-scale projects, such as the certified C compiler CompCert.

“The certified programming projects that have s\ucceeded so far remain impressive development efforts, requiring the work of many PhD-level experts over several years. The rigidity and complexity of proof assistants make these technologies difficult for beginners and non-specialized engineers to access,” says the researcher.

This project seeks to soften this barrier, fostering the malleability of proof assistants through three complementary axes: incrementality, graduality, and extensibility. “For each axis, we aim to contribute to both foundational and practical aspects, developing theoretical foundations as well as prototyping mechanisms and tools for the Rocq prover.”

“The Gallinette team is in charge of the development and evolution of the Rocq proof assistant, and is very active in the area of type theory, the underlying formalism behind these tools. Moreover, the idea is also to collaborate with other Inria teams working on type theory and proof 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 first-rate research being carried out in Chile, hosted at Universidad de Chile and an institute of international standing such as the Millennium Institute for Foundational Research on Data (IMFD)”.

He also points out that this is the result of a long international collaboration: “Quality research is rarely the product of an isolated genius, but rather the outcome of interactions and mutual enrichment with other people. In this case, it is the result of a thematic shift I began about 10 years ago, one I could not have achieved without the synergy with several people, especially Nicolas Tabareau, the researcher in charge of Gallinette at Inria, who was already an expert in these topics when I started to take an interest in them”.

“I am convinced that quality research can and must be developed from Chile, and that this type of distinction inspires new generations of scientists in our country”, states the academic.