Differential  $\lambda$-Calculus and Differential Linear Logic, 20 Years Later / $ \lambda $-calcul différentiel et logique linéaire différentielle, 20 ans après

Collection Differential $\lambda$-Calculus and Differential Linear Logic, 20 Years Later / $ \lambda $-calcul différentiel et logique linéaire différentielle, 20 ans après

In the early 2000’s, Ehrhard and Regnier introduced differential extensions of the λ-calculus and of Linear Logic: these give a syntactic counterpart to quantitative semantics, i.e. the interpretation of Linear Logic proofs as linear and continuous maps, and of functional programs as analytic maps, subject to Taylor expansion.

These seminal results have marked the starting point of a considerable amount of scientific contributions at the junction of computer science, logic and category theory. They allowed to elaborate a novel approximation theory of functional programs, refining order theoretic approaches with quantitative information. They provided valuable insights for the development of formal methods for probabilistic and differentiable programming. They were a major contribution to the categorical understanding of differentiation, unveiling the algebraic structure behind its various aspects. They participated to the rapid development of the bicategorical approach to denotational semantics, giving an abstract representation of computation paths at the 2-dimensional level.

This conference will be organized around invited talks reviewing the advances obtained since the advent of Differential λ-calculus and Differential Linear Logic, including the most recent ones, with special emphasis on the diversity of objects, techniques and fields of application. The programme will also include slots for participants to present their works in short contributed talks.


Organizer(s) Cerda, Rémy ; Guerrieri, Giulio ; Olimpieri, Federico ; Tasson, Christine ; Vaux Auclair, Lionel
Date(s) 13/05/2024 - 17/05/2024
linked URL https://conferences.cirm-math.fr/2980.html
Give feedback