Abstract

Probabilistic Coherent Spaces are fully abstract model of higher-order probabilistic computation interpreting types as convex sets and programs as analytic functions. After comparing this quantitative semantics with the well-known probabilistic power domain approach, we will see why our call-by-name approach prevents us from encoding some probabilistic algorithms. Then, we will focus on a probabilistic extension of Call-By-Push-Value that is well-suited for encoding probabilistic algorithms and that also enjoys full abstraction.

Video Recording