Verified Density Compilation for a Probabilistic Programming Language

Joseph Tassarotti, Jean Baptiste Tristan

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish (US)
Article number131
JournalProceedings of the ACM on Programming Languages
StatePublished - Jun 6 2023


  • compilers. probabilistic programming
  • formal verification

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality


Dive into the research topics of 'Verified Density Compilation for a Probabilistic Programming Language'. Together they form a unique fingerprint.

Cite this