Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
Bit Blasting Probabilistic Programs , volume=
2 Pith papers cite this work. Polarity classification is still indexing.
2
Pith papers citing it
years
2026 2verdicts
UNVERDICTED 2representative citing papers
Probabilistic programs of thought let LLMs produce many program variants from one generation by building a compact probabilistic representation of the token distribution.
citing papers explorer
-
Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
Continuous-Eris is a new separation logic that verifies exact samplers for the uniform, Gaussian, and Laplace distributions plus an exact real arithmetic library, with all proofs machine-checked in Rocq.
-
Probabilistic Programs of Thought
Probabilistic programs of thought let LLMs produce many program variants from one generation by building a compact probabilistic representation of the token distribution.