CONFERENCE

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

13 – 17 May, 2024

INTRANET FOR ORGANIZERS

Scientific Committee 
Comité scientifique 

Richard Blute (University of Ottawa)
Raphaëlle Crubillé (CNRS, Aix-Marseille Université)
Marcelo Fiore (University of Cambridge)
Damiano Mazza (CNRS, Université Sorbonne Paris Nord)
Michele Pagani (ENS de Lyon)

Organizing Committee
Comité d’organisation

Rémy Cerda (Aix- Marseille Université)
Giulio Guerrieri (University of Sussex)
Federico Olimpieri (Aix-Marseille Université)
Christine Tasson (ISAE-Supaero)
Lionel Vaux Auclair (Aix-Marseille Université)

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.

Au début des années 2000, Ehrhard et Regnier ont introduit des extensions différentielles du λ-calcul et de la logique linéaire: celles-ci offrent un pendant syntaxique à la sémantique quantitative, c’est-à-dire de l’interprétation des preuves de la logique linéaire comme des applications linéaires et continues, et des programmes fonctionnels comme des applications analytiques, sujettes au développement de Taylor.
Ces résultats séminaux ont marqué le début d’une quantité considérable de contributions scientifiques à la jonction de l’informatique théorique, de la logique et de la théorie des catégories. Ils ont permis de mettre au jour une théorie de l’approximation des programmes fonctionnels, raffinant avec des informations quantitatives les approches basées sur les ordres partiels. Ils ont guidé la mise au point de méthodes formelles pour la programmation probabiliste, et la programmation différentiable. Ils ont contribué de manière importante à l’étude catégorique de la différentiation, en révélant la structure algébrique derrière ses différents aspects. Ils ont participé au développement rapide de l’approche bicatégorique de la sémantique dénotationnelle, qui fournit au niveau 2-dimensionnel une abstraction des chemins d’exécution des
programmes.
Cette conférence sera structurée autour d’exposés de chercheuses et chercheurs invités, présentant les avancées obtenues depuis l’invention du λ-calcul différentiel et de la logique linéaire différentielle, jusqu’aux plus récentes. L’accent sera mis sur la diversité des objets, des techniques et des champs d’application. Le programme comprendra également des créneaux pour que les participants présentent leurs  ravaux, dans des exposés courts.

SPEAKERS

Pierre Clairambault (CNRS, Aix-Marseille Université)     Quantitative semantics in game models
Ugo Dal Lago (University of Bologna)    Reasoning Operationally about Probabilistic Higher-Order Programs
Thomas Ehrhard (CNRS, Paris Cité)    Coherent differentiation
Zeinab Galal (Bologna)   Stable species
Nicola Gambino (University of Manchester)    Generalized species
Brenda Johnson (Union College)   Differential Categories from Functor Calculus
Marie Kerjean (CNRS, Sorbonne Paris Nord)     Introduction to DiLL
Delia Kesner (Paris Cité)     Non-idempotent intersection types
Giulio Manzonetto (Paris Cité)     Taylor expansion and Böhm trees

Guy McCusker (Bath)     Weighted models
Paul-André Melliès (CNRS, Paris Cité)     Homotopical models
Jean-Simon Pacaud Lemay (Macquarie University)    Differential categories
Michele Pagani (ENS de Lyon)      Automatic differentiation
Luc Pellissier (Paris-Est Créteil)   Taylor expansion in proof nets
Christine Tasson (ISAE-Supaero)   Probabilistic coherence spaces

SPONSORS