Jean Goubault-Larrecq (LSV, ENS Cachan)

The powerdomain of continuous random variables

Résumé: We introduce the domain of continuous random variables (CRV) over a domain, as an alternative to Jones and Plotkin's probabilistic powerdomain. While no known Cartesian-closed category is stable under the latter, we show that the so-called thin (uniform) CRVs define a strong monad on the Cartesian-closed category of bc-domains. We also characterize their inequational theory, as (fair-)coin algebras. We apply this to solve a recent problem posed by M. Escard\'o: testing is semi-decidable for EPCF terms. CRVs arose from the study of the second author's (layered) Hoare indexed valuations, and we also make the connection apparent.