一句话：为 Stan 给出基于密度的操作语义，并设计可组合、自优化的 SlicStan，再保义翻译回 Stan。
Stan 是大规模概率编程的实用语言，但其块状语法牺牲了可组合性与灵活的用户自定义函数，且语言语义主要依赖实现直觉、缺乏形式化。本文对 Stan 进行形式化处理，提出可组合、自优化的概率编程语言 SlicStan。主要贡献包括：为 Stan 的核心子集给出基于密度的操作语义；设计 SlicStan 的语法与语义，借助信息流类型系统支持更好的代码复用与抽象；给出从 SlicStan 到 Stan 的保语义翻译过程。该工作以形式化语义和翻译正确性为核心，未报告实证评估。
Stan is a probabilistic programming language that has been increasingly used for real-world scalable projects. However, to make practical inference possible, the language sacrifices some of its usability by adopting a block syntax, which lacks compositionality and flexible user-defined functions. Moreover, the semantics of the language has been mainly given in terms of intuition about implementation, and has not been formalised. This paper provides a formal treatment of the Stan language, and introduces the probabilistic programming language SlicStan --- a compositional, self-optimising version of Stan. Our main contributions are (1) the formalisation of a core subset of Stan through an operational density-based semantics; (2) the design and semantics of the Stan-like language SlicStan, which facilities better code reuse and abstraction through its compositional syntax, more flexible functions, and information-flow type system; and (3) a formal, semantic-preserving procedure for translating SlicStan to Stan.
@article{paperbot690,
title = {Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic},
author = {Maria I. Gorinova and Andrew D. Gordon and Charles Sutton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290348}
}