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.
Proceed- ings of the ACM on Programming Languages (PACMPL) 3, POPL (1 1 2019), 36:1–36:29
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
verdicts
UNVERDICTED 3representative citing papers
ULLER's three independent semantics are unified as instances of monads, enabling modular addition of new semantics and translations between them.
Introduces independent subproblem inference and proves asymptotic convergence guarantees for hybrid MCMC algorithms defined via inference metaprogramming.
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.
-
NeSyCat: A Monad-Based Categorical Semantics of the Neurosymbolic ULLER Framework
ULLER's three independent semantics are unified as instances of monads, enabling modular addition of new semantics and translations between them.
-
Compositional Inference Metaprogramming with Convergence Guarantees
Introduces independent subproblem inference and proves asymptotic convergence guarantees for hybrid MCMC algorithms defined via inference metaprogramming.