Is differentiation as it appears in computer science the same as the one from standard mathematics ? In particular, can differentiation in linear logic compute on traditional objects of mathematics ?

Succeeding in finding such a smooth interpretation of differential linear logic requires to overcome several issues: finding a good category of reflexive spaces and understanding how to handle higher-order objects in functional analysis.

The first problem can be solved by exploiting the fact that polarities naturally appear in the theory of topological vector spaces; in particular the categories of spaces of distributions and their dual will provide an adequate example. For the second, I will review several solutions providing definitions for higher-order distributions.

This talk is based mainly on works in collaboration with Jean-Simon Lemay.