Raphaëlle Crubillé, The free exponential modality of probabilistic coherence spaces

Schedule

Abstract

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 λ-terms with entire functions, both mapping the convex set of their domain into the one of their codomain. This model is particularly precise in describing the observational equivalences between probabilistic functional programs. In this talk, we'll present the proof that the exponential modality is the free commutative comonad, giving a further mark of canonicity to the model.