一句话：提出 ProbCompCert：用 Coq 验证 Stan 子集概率编程语言编译器的关键遍，并发现 Stan 手册错误。
本文关注概率编程语言（PPL）编译器正确性问题。由于 PPL 的概率特性，编译器错误往往难以检测和修复，而验证其编译正确性又需要新方法，因为 PPL 中的某些变换与传统语言差异显著。作者提出 ProbCompCert，一个面向 Stan 语言子集的编译器，并在 Coq 证明助手中对若干关键编译遍进行形式化验证。论文介绍了用于验证这类概率变换的技术及其在 ProbCompCert 中的应用。验证过程中，作者还发现 Stan 语言参考手册中与某个关键语言构造的语义和实现相关的错误。
This paper presents ProbCompCert, a compiler for a subset of the Stan probabilistic programming language (PPL), in which several key compiler passes have been formally verified using the Coq proof assistant. Because of the probabilistic nature of PPLs, bugs in their compilers can be difficult to detect and fix, making verification an interesting possibility. However, proving correctness of PPL compilation requires new techniques because certain transformations performed by compilers for PPLs are quite different from other kinds of languages. This paper describes techniques for verifying such transformations and their application in ProbCompCert. In the course of verifying ProbCompCert, we found an error in the Stan language reference manual related to the semantics and implementation of a key language construct.
@article{paperbot1936,
title = {Verified Density Compilation for a Probabilistic Programming Language},
author = {Joseph Tassarotti and Jean-Baptiste Tristan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591245}
}