一句话：建立计数命题逻辑与概率事件 λ 演算的 Curry-Howard 对应，并以交集类型精确刻画概率行为。
论文研究如何将直觉主义计数命题逻辑通过 Curry-Howard 对应解释为概率计算类型系统。作者以概率事件 λ 演算为载体，该演算可模拟离散随机函数式程序的按名与按值求值；在此对应下，证明和类型不再保证有效性或终止性，而是揭示程序结果所服从的概率。为进一步精确刻画 λ 项的完整概率行为，作者为类型系统引入交集算子，得到一个能精确捕获概率语义的系统。该工作把 Borel 概率与证明论、类型论联系起来，为概率程序的逻辑化分析提供新框架。
We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.