Thomas Ehrhard (IRIF, Univ. Paris Diderot), Stable and measurable functions on positive cones: a model of probabilistic functional languages with continuous types

Programme

Résumé

Joint work with Michele Pagani and Christine Tasson

The Probabilistic Coherence Space (PCS) model provides a denotational semantics for probabilistic functional languages (with full recursion and recursive types) where programs are interpreted as power series with non-negative real coefficients. It has interesting properties (such as a Full Abstraction property), but seems to be essentially limited to discrete probabilities. To overcome this limitation, we replace PCSs with positive cones, which generalize them quite naturally, and power series with Scott-continuous functions which are "stable" in a sense that we will explain. A typical object of this new model is the cone of finite measures on the real line which seems impossible to represent as a PCS. Raphaëlle Crubillé has shown recently that this extension of the PCS model is conservative.