~/talk

Verified Density Compilation for a Probabilistic Programming Language

on YouTube 20m
Talkat PLDI 2023 · 2023-06-17..06-21· [compilers-and-language-design]

speakers

name:Joseph Tassarotti
website:https://cs.nyu.edu/~jt4767/
name:Jean-Baptiste Tristan
links:none on file

resources

video:https://youtu.be/FjZx1-fSADE
slides:none on file

summary

Provides a mechanized semantics for a Stan subset and verifies three density-compilation passes in Coq, producing ProbCompCert that connects to CompCert down to assembly. Proofs use forward simulation plus denotational reasoning to show transforms like reparameterization and additive-constant elimination preserve the posterior (up to normalization), and the effort uncovers an error in the Stan reference manual. Main limitation is that correctness is idealized over exact reals, not finite-precision floating-point.

AI-written summary · about

chapters (10)

  1. 0:00Introduction
  2. 1:07Project overview
  3. 3:17Density compilation in Stan
  4. 4:21Compiler specification
  5. 7:51Compiler correctness proof
  6. 9:56Reparameterization pass
  7. 12:25Additive constant optimization
  8. 14:33Floating point limits
  9. 15:57Conclusion
  10. 16:24Q&A

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.