Double indexed differential linear logic reconciling resources and differential operators
Simon Mirwasser
LIPN, Sorbonne Paris Nord
https://lipn.univ-paris13.fr/~mirwasser/
Date(s) : 17/04/2025 iCal
11h00 - 12h30
Graded Linear Logic is a central development of Linear Logic, quantifying the use of resources in proofs and programs. Differential Linear Logic, on the other hand, dualises this focus on resources by adding co-structural rules defining proof differentiation. In this paper we use the Laplace transform as the final building block to reconcile co-structural rules with graded exponential. We define a graded differential linear logic where structural and co-structural rules act on four different exponential connectives. Contrarily to previous work, this proof calculus goes higher-
order by including a promotion rule, and also provides a sound syntax for the recently introduced co-promotion rule. We provide two different models for this syntax: the first extends a previously known first-order model to higher order thanks to Köthe spaces, where the indices are either polynomials or linear partial differential operators. The second arises from the literature in functional analysis, the indices being Young functions and their convex conjugate.
Emplacement
I2M Luminy - TPR2, Salle de Séminaire 304-306 (3ème étage)
Catégories
