Verified Density Compilation for a Probabilistic Programming Language

Joseph Tassarotti; Jean Baptiste Tristan

doi:10.1145/3591245

Verified Density Compilation for a Probabilistic Programming Language

Joseph Tassarotti, Jean Baptiste Tristan

Computer Science

Research output: Contribution to journal › Article › peer-review

Abstract

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 language	English (US)
Article number	131
Journal	Proceedings of the ACM on Programming Languages
Volume	7
DOIs	https://doi.org/10.1145/3591245
State	Published - Jun 6 2023

Keywords

compilers. probabilistic programming
formal verification

ASJC Scopus subject areas

Software
Safety, Risk, Reliability and Quality

Access to Document

10.1145/3591245

Cite this

@article{f89c4a742c1d4c34adecba7171a476e2,

title = "Verified Density Compilation for a Probabilistic Programming Language",

abstract = "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.",

keywords = "compilers. probabilistic programming, formal verification",

author = "Joseph Tassarotti and Tristan, {Jean Baptiste}",

note = "Publisher Copyright: {\textcopyright} 2023 Owner/Author.",

year = "2023",

month = jun,

day = "6",

doi = "10.1145/3591245",

language = "English (US)",

volume = "7",

journal = "Proceedings of the ACM on Programming Languages",

issn = "2475-1421",

publisher = "Association for Computing Machinery (ACM)",

}

TY - JOUR

T1 - Verified Density Compilation for a Probabilistic Programming Language

AU - Tassarotti, Joseph

AU - Tristan, Jean Baptiste

PY - 2023/6/6

Y1 - 2023/6/6

N2 - 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.

AB - 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.

KW - compilers. probabilistic programming

KW - formal verification

UR - http://www.scopus.com/inward/record.url?scp=85161983127&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85161983127&partnerID=8YFLogxK

U2 - 10.1145/3591245

DO - 10.1145/3591245

M3 - Article

AN - SCOPUS:85161983127

SN - 2475-1421

VL - 7

JO - Proceedings of the ACM on Programming Languages

JF - Proceedings of the ACM on Programming Languages

M1 - 131

ER -

Verified Density Compilation for a Probabilistic Programming Language

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this