The Free Exponential Modality of Probabilistic Coherence Spaces

  (Michele Pagani)


Probabilistic coherence spaces yield a model of linear logic and
lambda-calculus with a linear algebra flavor. Formulas/types are
associated with convex sets of R+-valued vectors, linear logic proofs
with linear functions and lambda-terms with power series, both mapping
the convex set of their domain into the one of their codomain.

Previous results show that this model is particularly precise in
describing the observational equivalences between probabilistic
functional programs. In this talk, we introduce to the model and then
prove that the exponential modality is the free commutative comonad,
giving a further mark of canonicity to the model.