pith. sign in

arxiv: 2605.13526 · v2 · pith:SEQTVGXRnew · submitted 2026-05-13 · 💻 cs.LO

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

Markus de Medeiros , Puming Liu , Kwing Hei Li , Alejandro Aguirre , Lars Birkedal , Joseph Tassarotti This is my paper

Pith reviewed 2026-05-19 13:57 UTC · model grok-4.3

classification 💻 cs.LO
keywords separation logicexact samplingcontinuous distributionscomputable realsprobabilistic programsprogram verificationhigher-order logic
0
0 comments X p. Extension
pith:SEQTVGXR Add to your LaTeX paper What is a Pith Number? 
\usepackage{pith}
\pithnumber{SEQTVGXR}

Prints a linked pith:SEQTVGXR badge after your title and writes the identifier into PDF metadata. Compiles on arXiv with no extra files. Learn more

The pith

A higher-order separation logic verifies exact samplers for continuous distributions using computable reals.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper introduces Continuous-Eris, a higher-order separation logic built to prove that sampling algorithms generate exact samples from continuous distributions without relying on approximate floating-point arithmetic. This approach addresses the challenge of verifying programs that combine probabilistic choice, higher-order functions, and mutable state while producing samples to arbitrary precision via computable reals. A sympathetic reader would care because such verified exact methods avoid round-off errors that can compromise applications like differential privacy. The work demonstrates the logic by establishing correctness for samplers of the uniform, Gaussian, and Laplace distributions together with a supporting library of exact real arithmetic operations.

Core claim

Continuous-Eris is a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. Using Continuous-Eris, the authors establish the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples.

What carries the argument

Continuous-Eris, a higher-order separation logic that reasons about programs containing probabilistic choice, higher-order functions, and dynamically allocated mutable state to establish exact sampling properties for continuous distributions.

If this is right

  • The verified uniform, Gaussian, and Laplace samplers produce samples distributed exactly according to their target continuous distributions.
  • The exact real arithmetic library correctly supports operations on samples generated to arbitrary precision.
  • The logic accounts for the full combination of probabilistic choice with higher-order functions and mutable state in these algorithms.
  • Verification guarantees absence of approximation errors in the sampling process.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same logic could be used to verify samplers for additional continuous distributions not covered in the paper.
  • Verified exact samplers could strengthen security arguments in differential privacy mechanisms that add continuous noise.
  • Separation logic techniques shown here might extend to verification of other probabilistic programs that mix discrete and continuous elements.

Load-bearing premise

The soundness of Continuous-Eris holds with respect to the operational semantics of the underlying language that includes probabilistic choice, higher-order functions, and dynamically allocated mutable state.

What would settle it

A concrete execution trace or statistical test showing that one of the verified sampler programs produces samples whose distribution deviates from the target uniform, Gaussian, or Laplace distribution.

Figures

Figures reproduced from arXiv: 2605.13526 by Alejandro Aguirre, Joseph Tassarotti, Kwing Hei Li, Lars Birkedal, Markus de Medeiros, Puming Liu.

Figure 2
Figure 2. Figure 2: The maximum of two uniform [0, 1] samples. 2 Key Ideas To illustrate the key concepts of Continuous-Eris, we will verify the MaxU2 program in [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 10
Figure 10. Figure 10: The Negative Exponential sampler (E). L ε µ ≜ let (z, u) := E 0 in let sgn := rand 1 in Radd µ (Rscal ε (RofBZU (sgn, z, u))) [PITH_FULL_IMAGE:figures/full_fig_p021_10.png] view at source ↗
Figure 5
Figure 5. Figure 5: The language includes primitives for higher-order programming such as higher-order [PITH_FULL_IMAGE:figures/full_fig_p013_5.png] view at source ↗
read the original abstract

Most implementations of sampling algorithms for continuous distributions use floating-point numbers, which introduce round-off errors and approximations. These errors can be difficult to analyze, and can cause security issues when used in algorithms for differential privacy. An alternative is to use exact sampling algorithms based on computable reals, which can lazily generate the digits of a continuous sample to arbitrary precision. However, these algorithms are intricate, and implementing and using them involves a combination of semantically challenging language features, such as probabilistic choice, higher-order functions, and dynamically-allocated mutable state. In this paper we present Continuous-Eris, a higher-order separation logic for verifying the correctness of exact sampling algorithms for computable distributions. To demonstrate Continuous-Eris, we verify the correctness of computable samplers for the uniform, Gaussian, and Laplace distributions, as well as a library for exact real arithmetic for working with generated samples. All of the results in this paper have been verified in the Rocq proof assistant.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces Continuous-Eris, a higher-order separation logic for verifying exact sampling algorithms for computable continuous distributions. It demonstrates the logic by machine-checking in Rocq the correctness of samplers for the uniform, Gaussian, and Laplace distributions together with a library for exact real arithmetic, all in a language featuring probabilistic choice, higher-order functions, and mutable state.

Significance. If the soundness result holds, the work supplies a verified foundation for exact real sampling that avoids floating-point approximation errors, directly relevant to differential privacy and other security-critical uses. The machine-checked proofs in Rocq constitute a clear strength, as they discharge the central soundness claim against the operational semantics rather than leaving it as an unverified assumption.

minor comments (2)
  1. [§2] §2: the notation for the probabilistic choice operator is introduced twice with slightly different symbols; adopt a single consistent notation.
  2. The caption of Figure 3 could explicitly state the number of digits generated in the displayed sample to aid readers unfamiliar with exact reals.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the paper and their recommendation to accept. We are pleased that the referee recognizes the value of the machine-checked soundness proofs in Rocq and the relevance to applications such as differential privacy.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces Continuous-Eris, a higher-order separation logic, and uses it to verify samplers for uniform, Gaussian, and Laplace distributions plus an exact-real library. All claims, including the logic's soundness relative to the operational semantics of a language with probabilistic choice, higher-order functions, and mutable state, are discharged by machine-checked proofs in Rocq. No derivation step reduces to a fitted parameter, self-referential definition, or load-bearing self-citation; the formal artifact provides independent verification against external semantics rather than constructing results by construction from the inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The paper introduces a new program logic whose rules constitute the core axioms; the language semantics for probabilistic choice and state are taken as background assumptions. No numeric free parameters are present.

axioms (1)
  • domain assumption The operational semantics of the language featuring probabilistic choice, higher-order functions, and mutable state is correctly modeled by the logic.
    The logic is defined relative to this semantics; soundness of Continuous-Eris depends on it.
invented entities (1)
  • Continuous-Eris logic no independent evidence
    purpose: To enable verification of exact continuous samplers
    Newly defined higher-order separation logic; independent evidence would require external soundness proofs or applications beyond this paper.

pith-pipeline@v0.9.0 · 5712 in / 1296 out tokens · 65236 ms · 2026-05-19T13:57:37.450407+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

62 extracted references · 62 canonical work pages

  1. [1]

    and de Medeiros, Markus and Li, Kwing Hei and Gregersen, Simon Oddershede and Tassarotti, Joseph and Birkedal, Lars , title =

    Aguirre, Alejandro and Haselwarter, Philipp G. and de Medeiros, Markus and Li, Kwing Hei and Gregersen, Simon Oddershede and Tassarotti, Joseph and Birkedal, Lars , title =. Proc. ACM Program. Lang. , month = aug, articleno = 246, numpages = 33, keywords =. doi:10.1145/3674635 , abstract =

    work page doi:10.1145/3674635

  2. [2]

    Proceedings of the 2012 ACM conference on Computer and communications security , pages=

    On significance of the least significant bits for differential privacy , author=. Proceedings of the 2012 ACM conference on Computer and communications security , pages=

    work page 2012

  3. [3]

    A categorical approach to probability theory

    Giry, Mich \`e le. A categorical approach to probability theory. Categorical Aspects of Topology and Analysis. 1982

    work page 1982

  4. [4]

    John von Neumann, Collected Works , volume=

    Various techniques used in connection with random digits , author=. John von Neumann, Collected Works , volume=. 1963 , publisher=

    work page 1963

  5. [5]

    von Neumann , year =

    J. von Neumann , year =. Various techniques used in connection with random digits , booktitle =

    work page

  6. [6]

    Haselwarter and Joseph Tassarotti and Lars Birkedal , title =

    Simon Oddershede Gregersen and Alejandro Aguirre and Philipp G. Haselwarter and Joseph Tassarotti and Lars Birkedal , title =. Proc. doi:10.1145/3632868 , url =

    work page doi:10.1145/3632868

  7. [7]

    Karney, Charles F. F. , title =. ACM Trans. Math. Softw. , month = jan, articleno =. 2016 , issue_date =. doi:10.1145/2710016 , abstract =

    work page doi:10.1145/2710016 2016

  8. [8]

    Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science , articleno =

    Fernandes, Natasha and McIver, Annabelle and Morgan, Carroll , title =. Proceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science , articleno =. 2021 , isbn =. doi:10.1109/LICS52264.2021.9470718 , abstract =

    work page doi:10.1109/lics52264.2021.9470718 2021

  9. [9]

    Proceedings of the 2012 ACM Conference on Computer and Communications Security , pages =

    Mironov, Ilya , title =. Proceedings of the 2012 ACM Conference on Computer and Communications Security , pages =. 2012 , isbn =. doi:10.1145/2382196.2382264 , abstract =

    work page doi:10.1145/2382196.2382264 2012

  10. [10]

    Proceedings of the Forty-First Annual ACM Symposium on Theory of Computing , pages =

    Ghosh, Arpita and Roughgarden, Tim and Sundararajan, Mukund , title =. Proceedings of the Forty-First Annual ACM Symposium on Theory of Computing , pages =. 2009 , isbn =. doi:10.1145/1536414.1536464 , abstract =

    work page doi:10.1145/1536414.1536464 2009

  11. [11]

    Barthe, Gilles and Gaboardi, Marco and Grégoire, Benjamin and Hsu, Justin and Strub, Pierre-Yves , year = 2016, publisher =. A. doi:10.4230/LIPIcs.ICALP.2016.107 , booktitle =

    work page doi:10.4230/lipics.icalp.2016.107 2016

  12. [12]

    Dwork, Cynthia and Roth, Aaron , title =. Found. Trends Theor. Comput. Sci. , month = aug, pages =. 2014 , issue_date =. doi:10.1561/0400000042 , abstract =

    work page doi:10.1561/0400000042 2014

  13. [13]

    2019 , MONTH = Apr, DOI =

    M. 2019 , MONTH = Apr, DOI =

    work page 2019

  14. [14]

    A multiple-precision binary floating-point library with correct rounding, version 3.2.0 , url =

    MPFR , year =. A multiple-precision binary floating-point library with correct rounding, version 3.2.0 , url =

    work page

  15. [15]

    Iris from the ground up:

    Ralf Jung and Robbert Krebbers and Jacques. Iris from the ground up:. J. Funct. Program. , volume = 28, pages =. doi:10.1017/S0956796818000151 , timestamp =

    work page doi:10.1017/s0956796818000151

  16. [16]

    doi:10.5281/zenodo.11551307 , url =

    The Rocq Development Team , title =. doi:10.5281/zenodo.11551307 , url =

    work page doi:10.5281/zenodo.11551307

  17. [17]

    Sylvie Boldo and Catherine Lelay and Guillaume Melquiond , title =. Math. Comput. Sci. , volume =. 2015 , doi =

    work page 2015

  18. [18]

    Verified Foundations for Differential Privacy , year =

    de Medeiros, Markus and Naveed, Muhammad and Lepoint, Tancr\`. Verified Foundations for Differential Privacy , year =. Proc. ACM Program. Lang. , month = jun, articleno =. doi:10.1145/3729294 , abstract =

    work page doi:10.1145/3729294

  19. [19]

    Swaraj Dash and Younesse Kaddar and Hugo Paquet and Sam Staton , title =. Proc. 2023 , url =. doi:10.1145/3571239 , timestamp =

    work page doi:10.1145/3571239 2023

  20. [20]

    2016 , publisher=

    Perfect Simulation , author=. 2016 , publisher=

    work page 2016

  21. [21]

    Partially-Sampled Random Numbers for Accurate Sampling of Continuous Distributions , author=

    work page

  22. [22]

    CReal Library , author=

    work page

  23. [23]

    2003 , MONTH = May, KEYWORDS =

    M. 2003 , MONTH = May, KEYWORDS =

    work page 2003

  24. [24]

    Alexander Bagnall and Gordon Stewart and Anindya Banerjee , title =. Proc. 2023 , url =. doi:10.1145/3591220 , timestamp =

    work page doi:10.1145/3591220 2023

  25. [25]

    Li and Amal Ahmed and Steven Holtzen , title =

    John M. Li and Amal Ahmed and Steven Holtzen , title =. Proc. 2023 , url =

    work page 2023

  26. [26]

    Ho, Shing Hin and Wu, Nicolas and Raad, Azalea , title =. Proc. ACM Program. Lang. , month = jan, articleno =. 2026 , issue_date =. doi:10.1145/3776696 , abstract =

    work page doi:10.1145/3776696 2026

  27. [27]

    Approximate Relational Hoare Logic for Continuous Random Samplings , booktitle =

    Tetsuya Sato , editor =. Approximate Relational Hoare Logic for Continuous Random Samplings , booktitle =

    work page

  28. [28]

    Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL , booktitle =

    Michikazu Hirata and Yasuhiko Minamide and Tetsuya Sato , editor =. Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL , booktitle =. 2022 , url =. doi:10.1007/978-3-030-99461-7\_4 , timestamp =

    work page doi:10.1007/978-3-030-99461-7 2022

  29. [29]

    Tetsuya Sato and Alejandro Aguirre and Gilles Barthe and Marco Gaboardi and Deepak Garg and Justin Hsu , title =. Proc. 2019 , url =. doi:10.1145/3290351 , timestamp =

    work page doi:10.1145/3290351 2019

  30. [30]

    Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back , journal =

    Kevin Batz and Joost. Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back , journal =. 2025 , url =. doi:10.1145/3720429 , timestamp =

    work page doi:10.1145/3720429 2025

  31. [31]

    Guaranteed bounds for posterior inference in universal probabilistic programming , booktitle =

    Raven Beutner and C. Guaranteed bounds for posterior inference in universal probabilistic programming , booktitle =. 2022 , url =. doi:10.1145/3519939.3523721 , timestamp =

    work page doi:10.1145/3519939.3523721 2022

  32. [32]

    Millstein , title =

    Poorva Garg and Steven Holtzen and Guy Van den Broeck and Todd D. Millstein , title =. Proc. 2024 , url =. doi:10.1145/3656412 , timestamp =

    work page doi:10.1145/3656412 2024

  33. [33]

    32nd Annual

    Chris Heunen and Ohad Kammar and Sam Staton and Hongseok Yang , title =. 32nd Annual. 2017 , url =. doi:10.1109/LICS.2017.8005137 , timestamp =

    work page doi:10.1109/lics.2017.8005137 2017

  34. [34]

    Thomas Ehrhard and Michele Pagani and Christine Tasson , title =. Proc. 2018 , url =. doi:10.1145/3158147 , timestamp =

    work page doi:10.1145/3158147 2018

  35. [35]

    Fredrik Dahlqvist and Dexter Kozen , title =. Proc. 2020 , url =. doi:10.1145/3371125 , timestamp =

    work page doi:10.1145/3371125 2020

  36. [36]

    A domain theory for statistical probabilistic programming , journal =

    Matthijs V. A domain theory for statistical probabilistic programming , journal =. 2019 , url =. doi:10.1145/3290349 , timestamp =

    work page doi:10.1145/3290349 2019

  37. [37]

    Lew and Vikash K

    Mathieu Huot and Alexander K. Lew and Vikash K. Mansinghka and Sam Staton , title =. 38th Annual. 2023 , url =. doi:10.1109/LICS56636.2023.10175739 , timestamp =

    work page doi:10.1109/lics56636.2023.10175739 2023

  38. [38]

    A lambda-calculus foundation for universal probabilistic programming , booktitle =

    Johannes Borgstr. A lambda-calculus foundation for universal probabilistic programming , booktitle =. 2016 , url =. doi:10.1145/2951913.2951942 , timestamp =

    work page doi:10.1145/2951913.2951942 2016

  39. [39]

    Mitchell Wand and Ryan Culpepper and Theophilos Giannakopoulos and Andrew Cobb , title =. Proc. 2018 , url =. doi:10.1145/3236782 , timestamp =

    work page doi:10.1145/3236782 2018

  40. [40]

    An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages , booktitle =

    Daniel Huang and Greg Morrisett , editor =. An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages , booktitle =. 2016 , url =. doi:10.1007/978-3-662-49498-1\_14 , timestamp =

    work page doi:10.1007/978-3-662-49498-1 2016

  41. [41]

    Freer and Daniel M

    Cameron E. Freer and Daniel M. Roy , title =. Ann. Pure Appl. Log. , volume =. 2012 , doi =

    work page 2012

  42. [42]

    Ackerman and Cameron E

    Nathanael L. Ackerman and Cameron E. Freer and Daniel M. Roy , title =. J. 2019 , url =. doi:10.1145/3321699 , timestamp =

    work page doi:10.1145/3321699 2019

  43. [43]

    Computability of probability measures and Martin-Löf randomness over metric spaces , journal =

    Mathieu Hoyrup and Cristóbal Rojas , keywords =. Computability of probability measures and Martin-Löf randomness over metric spaces , journal =. 2009 , issn =. doi:https://doi.org/10.1016/j.ic.2008.12.009 , url =

    work page doi:10.1016/j.ic.2008.12.009 2009

  44. [44]

    Abbas Edalat , title =. Inf. Comput. , volume =. 2009 , doi =

    work page 2009

  45. [45]

    A domain-theoretic approach to Brownian motion and general continuous stochastic processes , booktitle =

    Paul Bilokon and Abbas Edalat , editor =. A domain-theoretic approach to Brownian motion and general continuous stochastic processes , booktitle =. 2014 , url =. doi:10.1145/2603088.2603102 , timestamp =

    work page doi:10.1145/2603088.2603102 2014

  46. [46]

    Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic , year =

    Marionneau, Virgil and Sassus Bourda, F\'. Modular Specifications and Implementations of Random Samplers in Higher-Order Separation Logic , year =. Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs , pages =. doi:10.1145/3779031.3779109 , abstract =

    work page doi:10.1145/3779031.3779109

  47. [47]

    Vernon A. Lee Jr. and Hans. Optimizing Programs over the Constructive Reals , booktitle =. 1990 , url =. doi:10.1145/93542.93558 , timestamp =

    work page doi:10.1145/93542.93558 1990

  48. [48]

    Towards an

    Hans. Towards an. Proceedings of the 41st. 2020 , url =. doi:10.1145/3385412.3386037 , timestamp =

    work page doi:10.1145/3385412.3386037 2020

  49. [49]

    Norbert Th. M. The. Computability and Complexity in Analysis, 4th International Workshop,. 2000 , url =. doi:10.1007/3-540-45335-0\_14 , timestamp =

    work page doi:10.1007/3-540-45335-0 2000

  50. [50]

    Implementing Real Numbers With

    Andrej Bauer and Iztok Kavkler , editor =. Implementing Real Numbers With. Proceedings of the Fourth International Conference on Computability and Complexity in Analysis,. 2007 , doi =

    work page 2007

  51. [51]

    Semantics of Exact Real Arithmetic , booktitle =

    Peter John Potts and Abbas Edalat and Mart. Semantics of Exact Real Arithmetic , booktitle =. 1997 , url =. doi:10.1109/LICS.1997.614952 , timestamp =

    work page doi:10.1109/lics.1997.614952 1997

  52. [52]

    Mart. Theor. Comput. Sci. , volume =. 1996 , url =. doi:10.1016/0304-3975(95)00250-2 , timestamp =

    work page doi:10.1016/0304-3975(95)00250-2 1996

  53. [53]

    Pietro Di Gianantonio , title =. Inf. Comput. , volume =. 1996 , doi =

    work page 1996

  54. [54]

    Simpson , editor =

    Alex K. Simpson , editor =. Lazy Functional Algorithms for Exact Real Functionals , booktitle =. 1998 , doi =

    work page 1998

  55. [55]

    1990 , url =

    Jean Vuillemin , title =. 1990 , url =. doi:10.1109/12.57047 , timestamp =

    work page doi:10.1109/12.57047 1990

  56. [56]

    and Tassarotti, Joseph and Birkedal, Lars , title =

    Li, Kwing Hei and Aguirre, Alejandro and Gregersen, Simon Oddershede and Haselwarter, Philipp G. and Tassarotti, Joseph and Birkedal, Lars , title =. Proc. ACM Program. Lang. , month = aug, articleno =. 2025 , issue_date =. doi:10.1145/3747514 , abstract =

    work page doi:10.1145/3747514 2025

  57. [57]

    , title =

    Wiedmer, E. , title =. Theoretical Computer Science , volume =

    work page

  58. [58]

    Haselwarter and Kwing Hei Li and Alejandro Aguirre and Simon Oddershede Gregersen and Joseph Tassarotti and Lars Birkedal , title =

    Philipp G. Haselwarter and Kwing Hei Li and Alejandro Aguirre and Simon Oddershede Gregersen and Joseph Tassarotti and Lars Birkedal , title =. Proc. 2025 , url =. doi:10.1145/3704877 , timestamp =

    work page doi:10.1145/3704877 2025

  59. [59]

    Haselwarter and Kwing Hei Li and Markus de Medeiros and Simon Oddershede Gregersen and Alejandro Aguirre and Joseph Tassarotti and Lars Birkedal , title =

    Philipp G. Haselwarter and Kwing Hei Li and Markus de Medeiros and Simon Oddershede Gregersen and Alejandro Aguirre and Joseph Tassarotti and Lars Birkedal , title =. Proc. 2024 , url =. doi:10.1145/3689753 , timestamp =

    work page doi:10.1145/3689753 2024

  60. [60]

    Patrick Billingsley , title =

    work page

  61. [61]

    doi:10.5281/zenodo.20114732 , url =

    de Medeiros, Markus and Liu, Puming and Li, Kwing Hei and Aguirre, Alejandro and Birkedal, Lars and Tassarotti, Joseph , title =. doi:10.5281/zenodo.20114732 , url =

    work page doi:10.5281/zenodo.20114732

  62. [62]

    2026 , eprint=

    Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic , author=. 2026 , eprint=

    work page 2026