一句话：为随机 λ-演算建立可靠且充分的指称语义与操作语义，统一高阶概率程序的语义框架。
本文研究随机 λ-演算的语义基础。该演算通过显式随机源刻画高阶概率程序。作者定义了指称语义与操作语义，并证明二者是可靠（sound）且充分（adequate）的，即操作行为与指称模型在观察等价意义下一致。该工作建立在以往用显式随机性推理高阶概率程序的成果之上，为随机 λ-演算提供统一的语义框架。关键结果是两类语义的对应性，为后续概率程序逻辑与验证奠定基础。
We define sound and adequate denotational and operational semantics for the stochastic lambda calculus. These two semantic approaches build on previous work that used an explicit source of randomness to reason about higher-order probabilistic programs.
@inproceedings{paperbot6242,
title = {Universal Semantics for the Stochastic λ-Calculus},
author = {Pedro H. Azevedo de Amorim and Dexter Kozen and Radu Mardare and Prakash Panangaden and Michael Roberts},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470747}
}