Invited Tutorial by Christine Tasson (Institut Supérieur de l'Aéronautique et de l'Espace, Toulouse): Linear Logic and probabilistic programming

A probabilistic program may generate different outputs according to the various probabilistic choices made during its execution. Thereby, probabilistic programs can be intuitively interpreted as probabilistic distributions (or more precisely as stochastic kernels that are parameterized distributions). The use of linearity in the semantics of probabilistic programs is particularly relevant. Indeed, sampling once a distribution and returning copies of the sample differs from sampling twice the same distribution and returning the pair of samples. Although stochastic kernels encode linearity and copying, they cannot account for higher-order probabilistic programming.

The quantitative effect at play in probabilistic programming has been a motivation from the very beginning of Linear Logic. The goal of this tutorial is to introduce Linear Logic through the prism of Probabilistic Programming. First, I will present probabilistic programming and inference. Then, I will describe two semantics of Linear Logic and of Higher-Order probabilistic programming for discrete and continuous distributions. These semantics account for sampling, linearity and copying.

Linear Logic stemmed from denotational investigations of the lambda-calculus and inspired powerful models, especially for probabilistic programming. This talk will illustrate the constant interactions between the design of Programming Languages, Logic and Semantics.