RESEARCH IN RESIDENCE
Differential calculus and analytic functors
Differential calculus and analytic functors
14 – 25 June, 2027
Participants
Marcelo Fiore (University of Cambridge)
Nicola Gambino (University of Manchester)
Martin Hyland (King’s College)
Christine Tasson (ISAE SUPAERO)
Lionel Vaux auclair (Aix-Marseille Université)
The purpose of this research in residence is to make two lines of investigation converge.
These concern, on the one hand, the recent extension of the differential calculus of species to a full model of differential linear logic by Fiore, Gambino, and Hyland; and, on the other, the mixed linear/cartesian operads of Fiore and the linear/cartesian substitution 2-monad of Hyland and Tasson). In this context, we are to work on the following.
(1) The approach of Fiore, based on PROPs, and the approach of Hyland, based on lax colimits, need to be formally related.
(2) A basic differential calculus founded upon a dual linear/cartesian typing system will be investigated.
(3) We will work on the conjecture that the 2-category of locally presentable categories is a model of differential linear logic extending that of Fiore.
(4) The relationship between the above and the recent work of Paré on a functorial difference calculus will be considered.
L’objectif de cette recherche en résidence est de faire converger deux axes d’investigation.
Il s’agit, d’une part, de l’extension récente du calcul différentiel des espèces à un modèle complet de logique différentielle linéaire par Fiore, Gambino et Hyland ; et, d’autre part, des opérades mixtes linéaires/cartésiennes de Fiore et de la 2-monade de substitution linéaire/cartésienne de Hyland et Tasson. Dans ce contexte, nous allons travailler sur les points suivants.
(1) L’approche de Fiore, basée sur les PROP, et celle de Hyland, basée sur les colimites laxistes, doivent être formellement reliées.
(2) Un calcul différentiel de base fondé sur un système de typage linéaire/cartésien dual sera étudié.
(3) Nous travaillerons sur la conjecture selon laquelle la 2-catégorie des catégories localement présentables est un modèle de logique linéaire différentielle étendant celui de Fiore.
(4) La relation entre ce qui précède et les travaux récents de Paré sur un calcul différentiel fonctorial sera examinée.
SPONSORS
