Reference. Type-Directed Discretization of Probabilistic Programs (Extended Version)

We study exact discretization as a semantics-preserving transformation for recursive, higher-order probabilistic programs with continuous distributions. We target programs where continuous values are compared against finitely many constants, so exact inference reduces to a discrete problem. Our central technical contribution is a non-local, type-directed analysis that infers where continuous values can be partitioned into finitely many observationally relevant regions, then rewrites sampling and comparison behavior over those regions. We call this transformation Slice. Because this construction is global and type-directed, correctness requires reasoning beyond the local syntax: we formalize the transformation and prove soundness for boolean queries using a coupling-style logical relations argument over operational semantics. As an application, transformed programs can be executed by discrete engines such as Dice, Roulette, and Storm. Our empirical evaluation shows two complementary strengths of Slice when paired with discrete backends: it enables exact inference for challenging continuous programs that lie beyond the reach of previous exact systems, and, on benchmarks where direct comparison is possible, it is competitive with state-of-the-art exact inference systems for continuous programs.

Cite

Cite as @wu-2026-type (helia, typst) · \cite{wu-2026-type} (LaTeX)
BibTeX
bibtex · 7 lines
@misc{wu-2026-type,
  author = {Katherine Wu and Jules Jacobs and Kevin Batz and Alexandra Silva},
  title = {Type-Directed Discretization of Probabilistic Programs (Extended Version)},
  year = {2026},
  month = {8},
  doi = {10.1145/3839534}
}
hayagriva YAML (typst)
yaml · 11 lines
wu-2026-type:
  type: misc
  title: Type-Directed Discretization of Probabilistic Programs (Extended Version)
  author:
  - Wu, Katherine
  - Jacobs, Jules
  - Batz, Kevin
  - Silva, Alexandra
  date: 2026-08
  serial-number:
    doi: 10.1145/3839534
Cites 52 works (1 here)
With notes (1)

Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming moy-2025-roulette

Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages. This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples.
PDF · DOI · pldb
External (51)
wu-2026-type reference entries/refs/wu-2026-type/wu-2026-type.hel