一句话：在概率相干空间模型中为 Call-By-Push-Value 加入随机选择，并证明其可靠性与完全抽象。
本文为 Levy 的 Call-By-Push-Value 引入概率扩展：仅添加一个封闭的“抛硬币”布尔原子表达式，得到可同时涵盖按名调用与按值调用、并支持递归（可能惰性）数据类型的语言，可视为 Scott PCF 的重要推广。作者在既有概率相干空间指称模型中解释该语言；该模型是全经典线性逻辑的范畴模型，将数据类型解释为资源 comonad 的 coalgebra。文章证明该语言的 adequacy 与 full abstraction，将先前结果推广到更现实且更强的编程语言。
We introduce a probabilistic extension of Levy's Call-By-Push-Value. This extension consists simply in adding a " flipping coin " boolean closed atomic expression. This language can be understood as a major generalization of Scott's PCF encompassing both call-by-name and call-by-value and featuring recursive (possibly lazy) data types. We interpret the language in the previously introduced denotational model of probabilistic coherence spaces, a categorical model of full classical Linear Logic, interpreting data types as coalgebras for the resource comonad. We prove adequacy and full abstraction, generalizing earlier results to a much more realistic and powerful programming language.