一句话：提出概率与非确定性 CBPV 语言，用两类类型绕开连续 domain 语义障碍，并证明可靠、充分与完全抽象。
论文针对高阶概率语言难以获得域论语义的问题：通常要求涉及的 domain 连续或拟连续，但已知方法无法做到。作者指出，若语言具有两类类型（值类型与计算类型），问题会自然消失：值类型在连续 dcpo 的笛卡尔闭范畴中解释，计算类型在对概率 powerdomain 函子封闭的范畴中解释；这一框架来自 Levy 的 call-by-push-value。基于此，论文定义一个 CBPV 语言，概率选择位于值类型内，而从值类型到计算类型的转换引入 demonic 非确定性。作者给出域论语义与操作语义，证明二者可靠且充分；进一步加入 statistical termination testers 与 parallel if 后，证明语言完全抽象，并说明这两个原语不可或缺。
There is no known way of giving a domain-theoretic semantics to higher-order probabilistic languages, in such a way that the involved domains are continuous or quasi-continuous. We argue that the problem naturally disappears for languages with two kinds of types, where one kind is interpreted in a Cartesian-closed category of continuous dcpos, and the other is interpreted in a category that is closed under the probabilistic powerdomain functor. Such a setting is provided by Paul B. Levy's call-by-push-value paradigm. Following this insight, we define a call-by-push-value language, with probabilistic choice sitting inside the value types, and where conversion from a value type to a computation type involves demonic non-determinism. We give both a domain-theoretic semantics and an operational semantics for the resulting language, and we show that they are sound and adequate. With the addition of statistical termination testers and parallel if, we show that the language is even fully abstract-and those two primitives are required for that.