Probabilistic coherence spaces are fully abstract for probabilistic PCF
Thomas Ehrhard, Christine Tasson, Michele Pagani · 2014
Probabilistic coherence spaces (PCoh) yield a semantics of higher-order probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in Pcoh characterizes the operational indistinguishability of programs in PCF with a random primitive.