Marie Kerjean (LIPN, Université Sorbonne Paris-Nord), DiLL est dans Laplace

Programme

Résumé

What do exponential maps and exponential connectives have in common? Well, more than we thought! This talk will describe several way in which they interact.

First, we will see how the exponential map helps construct the differentiation monad, a variant of the continuation monad where the unit is the differential. This monad has the nice property of characterizing quantitative programs, equal to their Taylor expansion.

We will also see how the exponential map gives a good interpretation of the co-digging, a fourth co-structural exponential rule missing to those added by Differential Linear Logic to Linear Logic. If time permits, we will look at its nice graded properties.

Finally, we will see how the exponential function defines the Laplace transformation, which transforms exponential connectives by turning distributions of type "!" into functions of type "?". We will see how this Laplace transformation turns co-structural rules into structural ones and explore its beautiful categorical properties.

This is joint work with Jean-Simon Pacaud Lemay.