Meeting with Thomas Ehrhard, co-recipient of the 2024 Alonzo Church Award

This year, the Alonzo Church Award ¹⁾, honored Thomas Ehrhard, CNRS research director at IRIF, and Laurent Regnier, professor at Aix-Marseille Université and member of the Institut de Mathématiques de Marseille. This award distinguishes five of their articles and recognizes the importance of their work on lambda calculus.
Meeting with Thomas Ehrhard, co-recipient of the 2024 Alonzo Church Award and research director at IRIF.

I have been working on topics related to linear logic since the early '90s. It was after my thesis that I started to become interested in this subject.

With Laurent Regnier, co-author of four of the five awarded papers, we shared the same office at the I2M (formerly the Institut de Mathématiques de Luminy) in Marseille. One day, I told him that I had noticed that it was possible to define the derive of lambda terms syntactically, and it convinced both of us. That's how we started working together from 2001 until the end of 2005, early 2006.

To begin with, the lambda calculus is a formalism at the interface of logic and computer science, as it allows for representing both proofs and programs. It is the origin of the Curry-Howard correspondence, which expresses a very close relationship between proofs and programs.

This work originates from denotational semantics invented in 1969, which provides a mathematical representation of programs and proofs, particularly those of linear logic born in 1986 thanks to the discovery by Jean-Yves Girard. Denotational semantics allows us to view proofs and programs within a framework that relates to what is known as linear algebra in mathematics. Therefore, in the late 1990s, I worked on models of linear logic, which are closely related to this intuition of linear algebra where it became natural to compute derivatives of programs, which was not intuitive until then. This is innovative because the operation of differentiation belongs to analysis, which is a branch of mathematics quite distant, at first glance, from logic. It is from this perspective, established by linear logic, that Laurent Regnier and I had the idea to introduce this differentiation operation into the lambda calculus and linear logic, since these are two very closely related formalisms.

The papers are all interconnected and develop the subject through different perspectives. They all take this idea of differentiation and try to draw exploitable consequences from it. We are in a truly operational computational framework, meaning that it can be implemented on a computer. We attempt to understand what it means to differentiate, which is an operation more related to a field quite distant from programming, and we reflect on what it means from a programming perspective.

The idea of computing program derivatives is not entirely new; it had already emerged in the 1980s for numerical analysis. Today, computing program derivatives is gaining importance again, especially in artificial intelligence, in machine learning with algorithms like backpropagation (the link between this notion of program derivative - in the sense of numerical analysis - and the one we introduced in logic with Laurent Regnier is still quite mysterious and needs further understanding). We are not the inventors of this idea, but we saw it spontaneously appear in a logical framework. This is what I appreciate in science, that things emerge and naturally impose themselves. It's not about importing something from domain A to domain B; rather, it's about recognizing the structures that naturally appear. In linear logic, differentiation somehow emerged in this way.

I am still working on these research topics; currently, I am supervising the thesis of Aymeric Walch, who is exploring a new perspective on the subject.

This work has provided theoretical tools in proof theory. In the theory of lambda calculus, it has introduced new theoretical tools, particularly regarding the theory of finite approximation of proofs and programs.
We were able to demonstrate new results and find simpler proofs of already known results. As for real applications in computer science, it essentially provides new intuitions, particularly on how programs interact with each other or rather how a program interacts with its argument, when it uses the latter to produce a result.
Semantics, my field of research, remains a fairly theoretical subject, but it maintains close links with the design and implementation of programming languages and program analysis, for example from the perspective of their complexity. We can hope that this differential approach will bring new ideas in the development of programming languages.

For me, this award acknowledges this collective effort, not only the work done with Laurent Regnier but also the entire work of a community, composed of an international group of researchers, primarily located in France, Italy, the United Kingdom, and Canada, who have taken up our ideas to develop new approaches and foster advancements.
This intense collaborative work has notably developed since 2015 within the IRN (International Research Network) of linear logic, which we initiated with my colleague Lorenzo Totora de Falco from the University of Roma Tre, in a CNRS research group that has been renewed and lasted for eight years.
I also want to emphasize the importance of the foundational work of Jean-Yves Girard, who provided the key concepts that are the basis of this work.

–

The awarded papers are as follows :

Thomas Ehrhard. “Finiteness spaces”. In: Mathematical Structures in Computer Science 15.4 (2005), pp. 615–646. doi: 10.1017/S0960129504004645

Thomas Ehrhard and Laurent Regnier. “The differential lambda-calculus”. In: Theoretical Computer Science 309.1-3 (2003), pp. 1–41. doi: 10.1016/S0304-3975(03)00392-X

Thomas Ehrhard and Laurent Regnier. “Uniformity and the Taylor expansion of ordinary lambda-terms”. In: Theoretical Computer Science 403.2-3 (2008), pp. 347–372. doi: 10. 1016/j.tcs.2008.06.001

Thomas Ehrhard and Laurent Regnier. “Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms”. In: Logical Approaches to Computational Barriers, Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30-July 5, 2006, Proceedings. Ed. by Arnold Beckmann et al. Vol. 3988. Lecture Notes in Computer Science. Springer, 2006, pp. 186–197. doi: 10.1007/11780342_20

Thomas Ehrhard and Laurent Regnier. “Differential interaction nets”. In: Theoretical Computer Science 364.2 (2006), pp. 166–195. doi: 10.1016/j.tcs.2006.08.003