Marie Kerjean (IRIF), Smooth models of Differential Linear Logic



While Linear Logic has been from the start strongly tied to algebra, it is only the later introduction of Differential Linear Logic (DiLL) that suggested similar ties with analysis. DiLL extends Linear Logic with differentiation, an operation which extracts a linear proof from a non-linear one. In this talk, I will present several models of DiLL interpreting formulas as topological vector spaces and proofs as smooth functions, thus strenghtening the analogy with (functional) analysis. I will explain a work with Y. Dabrowski highlighting how with a well chosen Mackey duality and under a specific completeness assumption, the multiplicative disjunction of LL corresponds to epsilon product of Schwartz. As opposed to the purely algebraic case, we can identify this connective with a well-known mathematical object. I will present a classical polarized model of a version of DiLL without promotion, where formulas are interpreted as nuclear spaces and where exponentials are interpreted as spaces of distributions. This models argues for a smooth Differential Linear Logic which, I will explain, hints for a type theory of differential equations.