2024 Alonzo Church Award for Outstanding Contributions to Logic and Computation

The European Association for Computer Science Logic (EACSL), the European Association for Theoretical Computer Science (EATCS), and the ACM Special Interest Group for Logic and Computation (SIGLOG) are pleased to announce that the 2024 Alonzo Church Award for Outstanding Contributions to Logic and Computation is presented jointly to

Thomas Ehrhard and Laurent Regnier

for giving a logical and computational account of differentiation, bringing Taylor expansion to the Curry-Howard correspondence, which had a major impact on programming language semantics.

The awardee papers are:

• 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

The nominated papers introduced differential lambda-calculus and differential linear logic, together with the Taylor expansion of terms and proofs. The extension of the lambda-calculus with a derivation operator gives a syntactic account of differentiation, which reconciles the computational, logical, and algebraic notions of linearity. This allowed recasting Taylor expansion as a transformation of programs into superpositions of multilinear approximants, each capturing a finite computational behavior. The Taylor expansion has provided new and simpler proof methods to characterize the denotational and operational properties of programs. Differential linear logic similarly extends linear logic with new rules reflecting the logical structure of differentiation, yielding a sharper understanding of logical interaction. Differential linear logic has directly inspired unexpectedly effective accounts of differentiation in category theory, and strongly influenced current advances in higher-dimensional models of logic and computation. Differentiation has been instrumental in the design of new models of non-deterministic, probabilistic, quantum, or concurrent computation. After 20 years of intensive use, the concepts introduced in the awarded papers are time-tested and precious additions to the standard toolbox of the working linear logicians and programming language semanticists.

The Alonzo Church Award for Outstanding Contributions to Logic and Computation was established in 2015 by the ACM Special Interest Group for Logic and Computation (SIGLOG), the European Association for Theoretical Computer Science (EATCS), the European Association for Computer Science Logic (EACSL), and the Kurt Gödel Society (KGS). The award is for an outstanding contribution represented by a paper or small group of papers within the past 25 years.

The 2024 award will be presented at the Thirty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) which is scheduled to take place in Tallinn, Estonia during 8–11 July 2024.

The 2024 Alonzo Church Award Committee consists of the following five members: Thomas Colcombet, Anuj Dawar, Mariangiola Dezani, Marcelo Fiore, and Igor Walukiewicz (chair).