Michele Pagani (Univ. Paris 13), Syntax vs Semantics: a quantitative bridge



Since its inception, various models of Linear Logic have been defined in categories of vector spaces (more generally modules) and linear functions. These models provide semantics of quite expressive higher-order functional programming languages, where the denotation of a program is given by a matrix.

A natural question then arises -- What is the computational meaning of the scalars appearing in such matrices?, Can we recover from them some operational behavior that is hidden in the standard (domain based) semantics?

Danos & Ehrhard give a first positive answer in the specific case of probabilistic coherence spaces. We address the question in a more general setting, providing a general construction of adequate models parametrized by a continuous semiring of scalars. We show how specific instances of such a semiring allow to compare programs not only with respect to "what they can do", but also in "how many steps" or "with what resources" or in "how many ways" (for non-determistic calculi) or "with what probability" (for probabilistic calculi).

(This is a joint work with Jim Laird (Bath), Giulio Manzonetto (Paris 13) and Guy McCusker (Bath))