Pith. sign in

REVIEW 3 major objections 4 minor 46 references

Reactive Probabilistic Programming

T0 review · 3 major / 4 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read ProbZelus is the first synchronous probabilistic programming language: it puts Bayesian inference inside unbounded reactive streams while keeping memory bounded for a large class of models.

desk verdict ProbZelus is the real deal as the first synchronous PPL; the practical bounded-memory results hold up, but the advertised guarantee is informal and needs either a proof or a more careful statement. read the letter →

arxiv 1908.07563 v2 pith:OP3HES77 submitted 2019-08-20 cs.PL

Guillaume Baudart , Louis Mandel , Eric Atkinson , Benjamin Sherman , Marc Pouzet , Michael Carbin This is my paper · ORCID
classification cs.PL MSC 68N1868Q55
keywords probabilisticprogrammingsynchronouslanguagesstreaminginferencedelayedsamplingparticlefilteringBayesiandataflowinference-in-the-loop
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

ProbZelus is a synchronous probabilistic programming language: it extends the synchronous data-flow style with sample, observe, and infer, so a control program and a Bayesian model of its environment live in the same source. The paper gives the language a measure-theoretic co-iterative semantics, separates deterministic from probabilistic expressions by a kind system, and compiles both into a first-order functional core with a proof that the semantics is preserved. On the inference side, it reworks delayed sampling into a pointer-minimal streaming algorithm, called streaming delayed sampling, that keeps live memory constant over infinite streams for state-space models and other models with bounded dependency chains. The evaluation shows that SDS reaches the accuracy of thousands of particles with one particle on conjugate models, and completes benchmarks such as SLAM and multi-target tracking where a particle filter times out. The claim matters because safety-critical control software could then run Bayesian inference in the loop while retaining the bounded-resource guarantees that synchronous languages are chosen for.

What carries the argument

The load-bearing mechanism is the co-iterative semantics of stream functions, in which a program is an initial state plus a transition function; the probabilistic variant returns a measure over pairs (value, next state), adapted from measure-theoretic semantics of probabilistic programs. Around this semantics the paper builds a compiler to the first-order functional language $\mu$F, and re-implements delayed sampling with a pointer-minimal graph: initialized nodes keep only a parent pointer, marginalized nodes only a child pointer, so nodes that the program no longer references can be garbage-collected. The graph is what carries symbolic exact inference, and the pointer discipline is what turns an algorithm whose memory grew with the number of random variables into one whose memory stays flat for bounded-dependency models.

What would settle it

Instrument the published SDS implementation on the Robot benchmark from Section 2 and plot the number of live heap words per step for 10,000 steps; the bounded-memory claim stands only if that curve is flat. A linear increase in live heap words with step number would refute the central guarantee.

Watch

Extended reading notes

Core claim

The paper's central claim is that probabilistic programming can be embedded in the synchronous data-flow paradigm without losing its resource guarantees. ProbZelus is claimed to be the first synchronous probabilistic programming language: it extends the Zelus language with sample, observe, and infer, gives probabilistic stream functions a measure-theoretic co-iterative semantics, and separates deterministic from probabilistic code by a kind system so that infer is the only bridge from the probabilistic world back to the deterministic one. The paper proves that compilation from ProbZelus to the first-order language $\mu$F preserves this semantics, and on the inference side it contributes streaming delayed sampling, a pointer-minimal version of delayed sampling that keeps partial exact inference over infinite streams in bounded memory. Evaluation on Kalman, robot, SLAM, and multi-target tracking benchmarks demonstrates that SDS reaches target accuracy with far fewer particles than a particle filter, and on conjugate state-space models it is exact with a single particle.

Load-bearing premise

The bounded-memory guarantee of SDS rests on an informal condition—the model keeps only bounded dependency chains between variables—that the paper neither defines formally, proves, nor checks statically; if that condition cannot be made precise, the headline guarantee has no clear scope.

Editorial extensions

If this is right

  • ProbZelus programs can run Bayesian inference at every clock tick and feed the inferred distribution back into the controller, all in the same source.
  • For state-space models with conjugate updates, SDS is exact with one particle, so the accuracy-versus-particle-count tradeoff disappears for that class.
  • SDS keeps live memory constant on non-terminating streams for models with bounded dependency chains, whereas the original delayed sampling grows linearly.
  • On SLAM and multi-target tracking, SDS reaches target accuracy while a particle filter times out, widening the set of feasible online inference problems.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper, the bounded-dependency condition could likely be turned into a static analysis on ProbZelus programs, so compilers could reject programs that violate the memory bound instead of relying on the programmer to write them.
  • Because SDS is defined on the compiled $\mu$F core, the same streaming inference engine could be reused by other front-ends that lower into that core.
  • The pointer-minimal graph idea applies beyond synchronous languages: any long-running online Bayesian inference task that must forget old latent variables could use the same pruning discipline.
  • The paper leaves continuous-time probabilistic models open; combining SDS with the base language's support for ordinary differential equations is a natural extension.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper presents ProbZelus, an extension of the synchronous data-flow language Zelus with probabilistic constructs (sample, observe, infer). It contributes a co-iterative measure-based semantics for probabilistic stream functions, a type system separating deterministic and probabilistic expressions, and a semantics-preserving compilation to a first-order functional language µF. On the inference side, it adapts particle filtering to stateful stream processes and proposes two delayed-sampling variants: BDS, which resets the symbolic graph each step, and SDS, a pointer-minimal graph representation intended to keep memory bounded on infinite streams for models with bounded dependency chains. The paper reports an open-source implementation and an empirical evaluation on seven benchmarks, showing that SDS achieves exact or near-exact inference with few particles and large speedups over particle filtering.

Significance. If the claims hold, ProbZelus is a notable step: it is the first synchronous probabilistic programming language and the first to bring probabilistic inference into the feedback loop of safety-critical reactive systems while retaining the bounded-resource execution style of synchronous languages. The measure-theoretic semantics and the typed compilation provide a clean foundation, and the evaluation is broad, including benchmarks where particle filtering times out. The paper ships an open-source implementation and an artifact, which is a strength. However, the central bounded-memory guarantee for SDS is not established at the same formal level as the rest of the paper: the class of models with 'bounded chains of dependencies' is described informally and the memory measurements cover only 500 steps. This is the main weakness, and it matters because bounded memory is the key practical motivation for the work.

major comments (3)
  1. [Section 5.3, Limitations] The headline claim that SDS provides 'efficient, bounded memory inference' (Abstract and Section 1) is not formally established. Section 5.3 defines the applicable class only informally: models that 'maintain bounded chains of dependencies between variables' are said to run in bounded memory, but no formal definition of this class is given, no theorem states that the size of the delayed-sampling graph is bounded per particle for programs in this class, and no static or dynamic check is provided to reject programs like p1 and p2. The empirical memory plots in Figures 26 and 28 show flat heap for 500 steps, but this does not establish an asymptotic bound, particularly for benchmarks such as Robot whose sporadic GPS observations condition when dependency chains are pruned. I recommend either (a) formalizing the bounded-chain condition, proving that SDS keeps the graph size bounded for programs satisfying it, and providing a checkable criterion, or (b) weakening the abstract and introduction claims to describe the memory behavior as empirically demonstrated for the evaluated benchmarks.
  2. [Section 4.3, Semantics equivalence] The Theorem in Section 4.3 states that compilation from ProbZelus to µF is semantics-preserving for all expressions, but the proof only works out the case of sample(e) and says the rest follows by induction. Since the equivalence of the co-iterative semantics and the compiled µF semantics underpins the presentation of all inference algorithms in Section 5, the journal version should supply the complete induction, or at least a detailed sketch covering present, reset, local recursive equations, observe, and infer; the current one-case proof is too thin for a load-bearing theorem.
  3. [Section 6 and Appendix F.3] The text states 'In all cases, the inference runs in bounded memory (see Appendix F.3)', but Appendix F.3 only reports empirical measurements over 500 steps, and for the multi-target tracker the memory is random. This is an overclaim: the measurements cannot establish an asymptotic guarantee, and the sentence should be qualified to say that memory is observed to stabilize over the measured horizon for the benchmarks tested.
minor comments (4)
  1. [Appendix E, Artifact] There is a typo: 'passord' should be 'password', and 'The credential to log into' should be 'The credentials to log into'.
  2. [Section 6, Accuracy methodology] The accuracy criterion |log(P90%(loss)) − log(loss_target)| < 0.5 is not fully explained; please clarify whether P90% is the 90th percentile of loss over runs and justify the chosen threshold.
  3. [Section 5.3, p1 and p2] The two counterexamples p1 and p2 are described verbally as forming unbounded chains; a small diagram or an explicit expression for the graph size as a function of the number of steps would make the boundary of the class easier to verify and would strengthen the presentation.
  4. [Section 3.3 and Appendix A.3] The discussion of the alternative Scott-style semantics in Appendix A.3 is interesting but very brief; a sentence stating why this alternative is rejected beyond 'not practical in a reactive context' would help the reader.

Circularity Check

0 steps flagged · score 1.0 of 10

No material circularity found: the semantic, compilation, and inference claims are either proved in the paper (inductive equivalence theorem) or honestly adapted from external prior work (Staton's measure semantics; Murray et al.'s delayed sampling); the informal 'bounded dependency chains' scope of the streaming delayed sampling guarantee is a rigor gap, not a derivation that reduces to its own…

full rationale

The derivation chain is largely self-contained, and where it leans on prior work, that work is external or carries independent content. The co-iterative semantics of deterministic streams is cited to Caspi and Pouzet [12] (an author's earlier work), but the paper's actual contribution, the measure-based co-iterative semantics of probabilistic stream functions, is new and explicitly 'adapted from [39]' (Staton), an external published semantics. The compilation to µF is accompanied by a theorem stating ⟦e⟧ = ⟦C(e)⟧ for every expression, with a proof by induction whose sample case is spelled out, so the compiled semantics is derived rather than assumed. Delayed sampling is taken from Murray et al. [31] (Section 5.2: 'value, assume, and observe ... defined in [31]'), and the streaming redesign (SDS) is presented with a concrete mechanism (pointer-minimal graph, pruning of unreferenced nodes), honest counterexamples p1 and p2, and empirical memory curves (Figures 5, 26, 28); it is not a renamed known result, and no fitted parameter is renamed as a prediction. The one self-referential element is the evaluation protocol (Section 6: 'the baseline is the median loss of SDS at 1000 particles'), but that is a benchmarking target, not a derivation of SDS's efficiency claims, and the exactness claims for Beta-Bernoulli, Kalman-1D, and Robot rest on conjugacy and measured accuracy rather than on the target definition. The skeptic's concern is real but does not amount to circularity: Section 5.3 scopes the bounded-memory guarantee to 'models ... that only maintain bounded chains of dependencies between variables', and that class is left informal, with no formal definition, no proof of the memory bound, and no static check rejecting p1 and p2, while the 500-step memory plots cannot by themselves establish an asymptotic bound. That is an unproven, informally delimited guarantee (a rigor and correctness risk), not an input made equivalent to its output by construction, and the paper candidly discloses the limitation and offers a user-level mitigation (eval), pointing away from any attempt to pass the hypothesis off as a theorem. The 'first synchronous probabilistic programming language' claim is supported by the construction in the paper and by critical comparison with Lutin, ProPL, and CTPPL in Section 7, not by self-citation.

Assumptions & free parameters 0 free parameters · 4 assumptions · 4 invented entities

The core language design and inference algorithm do not depend on fitted numerical parameters. The main assumptions are the synchronous abstraction, the measure-theoretic semantics framework, and the informal bounded-dependency-chain condition that delimits SDS's memory guarantee.

assumptions (4)
  • domain assumption The synchronous abstraction: computations and communications are instantaneous and paced on a global clock.
    The entire language is based on this model, introduced in Section 1 and used in the co-iterative semantics.
  • standard math Measure-theoretic semantics of probabilistic programs as in Staton [39].
    The probabilistic semantics of muF follows Staton's commutative semantics; used in Sections 3.3 and 4.3.
  • domain assumption Conjugacy relationships between distributions support closed-form marginalization in delayed sampling.
    The delayed sampling algorithm relies on conjugacy, e.g., Beta-Bernoulli and Gaussian-Gaussian, to compute exact posteriors. This is standard Bayesian analysis but is not proven in the paper.
  • ad hoc to paper Bounded-memory execution is guaranteed for models whose dependency chains are bounded.
    Section 5.3 asserts this large class of models without a formal definition or proof. The Limitations paragraph gives counterexamples, p1 and p2, that fall outside the class.
invented entities (4)
  • ProbZelus independent evidence
    purpose: A synchronous probabilistic programming language combining dataflow control with sample, observe, and infer.
    Open source implementation at github.com/IBM/probzelus and benchmark evaluations in Section 6.
  • muF independent evidence
    purpose: First-order functional intermediate language with probabilistic operators, target of the semantics-preserving compilation.
    Used as the compilation target and as the basis for the inference algorithm definitions.
  • Streaming Delayed Sampling (SDS) independent evidence
    purpose: A pointer-minimal delayed sampling algorithm intended to run in bounded memory over infinite streams.
    Implemented and evaluated on benchmarks; memory measurements in Appendix F.3 confirm constant memory on the tested models.
  • Bounded Delayed Sampling (BDS) independent evidence
    purpose: A simpler delayed sampling variant that resets the graph at each time step to guarantee bounded memory.
    Implemented and compared in the evaluation.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Reactive Probabilistic Programming." pith.science (2026). https://pith.science/paper/OP3HES77

@misc{pith2026190807563,
  author       = {Pith},
  title        = {Pith review of: Reactive Probabilistic Programming},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/OP3HES77}},
  note         = {Machine review of arXiv:1908.07563}
}
read the original abstract

Synchronous modeling is at the heart of programming languages like Lustre, Esterel, or Scade used routinely for implementing safety critical control software, e.g., fly-by-wire and engine control in planes. However, to date these languages have had limited modern support for modeling uncertainty -- probabilistic aspects of software's environment or behavior -- even though modeling uncertainty is a primary activity when designing a control system. In this paper we present ProbZelus the first synchronous probabilistic programming language. ProbZelus conservatively provides the facilities of a synchronous language to write control software, with probabilistic constructs to model uncertainties and perform inference-in-the-loop. We present the design and implementation of the language. We propose a measure-theoretic semantics of probabilistic stream functions and a simple type discipline to separate deterministic and probabilistic expressions. We demonstrate a semantics-preserving compilation into a first-order functional language that lends itself to a simple presentation of inference algorithms for streaming models. We also redesign the delayed sampling inference algorithm to provide efficient streaming inference. Together with an evaluation on several reactive applications, our results demonstrate that ProbZelus enables the design of reactive probabilistic applications and efficient, bounded memory inference.

Figures

Figures reproduced from arXiv: 1908.07563 by the authors.

Figure 2
Figure 2. Kalman filter for the robot example. Variables are either latent (white, e.g., state x) or observed (gray, e.g., acceleration a). The position p is only sporadically observed. process that computes the stream u of commands. It is writ￾ten as two mutually recursive equations that define x_dist from u and u from the previous value of x_dist. The command u is set to the initial command uo at the first time step, and is… view at source ↗
Figure 3
Figure 3. Particle filter (PF) and streaming delayed sampling (SDS) performances for the robot example of [PITH_FULL_IMAGE:figures/full_fig_p004_3.png] view at source ↗
Figure 4
Figure 4. Evolution of the delayed sampling graph for the model of [PITH_FULL_IMAGE:figures/full_fig_p005_4.png] view at source ↗
Figures from the paper (19 more)
Figure 5
Figure 5. Figure 5: Delayed sampling (DS) and streaming delayed sampling (SDS) memory consumption in thousands of live words in the heap per steps for the robot example. design controls by enforcing a separation between the se￾mantics of probabilistic and deterministic execution. In this …
Figure 6
Figure 6. Figure 6: Semantics of deterministic expressions. The type T dist∗ is a subtype of T dist that represents dis￾tributions known to have a density, i.e., discrete distribu￾tions (w.r.t. the counting measure) and a subset of continuous distributions (w.r.t. the Lebesgue measure). I…
Figure 7
Figure 7. Figure 7: (the complete semantics is in [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]
Figure 8
Figure 8. Figure 8: Delayed sampling sampler. Expressions return a pair (symbolic expression, weight). In addition to the importance weight, each particle exploits conjugacy relationships between pairs of random variables to maintains a graph: a Bayesian network representing closed￾form d…
Figure 9
Figure 9. Figure 9: One step of the robot example of [PITH_FULL_IMAGE:figures/full_fig_p011_9.png]
Figure 10
Figure 10. Figure 10: Execution time comparison when 90% of 1000 runs reach an accuracy similar to the baseline (median accuracy of SDS with 1000 particles) after 500 steps. The number of particles required to reach this accuracy is shown on top of the bars. The error bars show the 10th an…
Figure 11
Figure 11. Figure 11: Execution time comparison with two different baselines: median accuracy of PF with 2000 and 4000 parti￾cles, respectively. Reactive Languages with Uncertainty. Lutin is a language for describing non-deterministic reactive systems for test￾ing and simulation [36], but …
Figure 12
Figure 12. Figure 12: Typing with deterministic and probabilistic kinds. we require sub-expressions to be deterministic, that is, in pairs, operator applications (including sample, factor, and observe), function calls, and the condition of a if/then/else. These restrictions simplify the pr…
Figure 13
Figure 13. Figure 13: Co-iterative semantics of deterministic ProbZelus programs. For local definitions each initialized variable is defined in a subsequent equation, i.e., {xi }1..k ∩ {yj }1..n = {xi }1..k . 18 [PITH_FULL_IMAGE:figures/full_fig_p018_13.png]
Figure 14
Figure 14. Figure 14: Co-iterative semantics of probabilistic ProbZelus expressions (i.e., kindOf (e) = P). For local definitions each initialized variable is defined in a subsequent equation, i.e., {xi }1..k ∩ {yj }1..n = {xi }1..k . 19 [PITH_FULL_IMAGE:figures/full_fig_p019_14.png]
Figure 15
Figure 15. Figure 15: Typing of µF with deterministic and probabilistic kinds. {[let f = e]}γ = γ [{[e]}γ /f ] {[d1 d2]}γ = let γ1 = {[d1]}γ in {[d2]}γ1 {[e]}γ = λU . δ⟦e⟧γ (U ) if kindOf (e) = D {[e1(e2)]}γ = λU . (⟦e1⟧γ (⟦e2⟧γ ))(U ) {[let p = e1 in e2]}γ = λU . ∫ T {[e1]}γ (du){[e2]}γ +…
Figure 17
Figure 17. Figure 17: Memory allocation, i.e., initialization for the µF step functions. The infer operator takes a transition function fun s -> e and an array of pairs (state, weight) S of size N which repre￾sents the distribution of possible states across the particles. ⟦infer(fun s -> e…
Figure 18
Figure 18. Figure 18: Compilation of ProbZelus to µF . ⟦let f = e⟧γ = γ [{[e]}γ,1/f ] if kindOf (e) = P {[e]}γ,w = (⟦e⟧γ ,w) if kindOf (e) = D {[e1(e2)]}γ,w = let v2 = ⟦e2⟧γ in ⟦e1⟧γ (v2,w) {[if e then e1 else e2]}γ,w = if ⟦e⟧γ then {[e1]}γ,w else {[e2]}γ,w {[let p = e1 in e2]}γ,w = let v1…
Figure 19
Figure 19. Figure 19: Importance sampler. Probabilistic expressions return a pair (value, weight). sample draws a sample from a distribution, factor and observe update the weight. The weights of the particles are multiplied at each step and never reset. In other words, the inference report…
Figure 20
Figure 20. Figure 20: Screenshots of the execution of the SLAM with the PF and SDS inferences. For each screenshot, the top line shows the map, and the blue circle the exact position of the robot. The lower line represents the inferred map where the gray level indicates the probability for…
Figure 21
Figure 21. Figure 21: Accuracy as a function of the number of particles. 10−1 100 101 102 103 104 105 1 10 100 1000 10000 Beta-Bernoulli Latency 10−1 100 101 102 103 104 105 1 10 100 1000 10000 Execution time of 500 steps in ms (log scale) Gaussian-Gaussian Latency 10−1 100 101 102 103 104…
Figure 23
Figure 23. Figure 23: Accuracy as a function of the number of particles. 101 102 103 104 105 106 1 10 100 1000 10000 Robot Latency 10−1 100 101 102 103 104 105 106 1 10 100 1000 10000 Execution time of 500 steps in ms (log scale) SLAM Latency 101 102 103 104 105 106 1 10 100 1000 10000 Num…
Figure 25
Figure 25. Figure 25: Runtime performance at each step of a run. 101 102 0 50 100 150 200 250 300 350 400 450 500 Beta-Bernoulli Ideal Memory 101 102 0 50 100 150 200 250 300 350 400 450 500 Thousands of words in heap (log scale) Gaussian-Gaussian Ideal Memory 101 102 103 104 0 50 100 150 …
Figure 27
Figure 27. Figure 27: Runtime performance at each step of a run. 101 102 103 104 0 50 100 150 200 250 300 350 400 450 500 Robot Ideal Memory 101 102 0 50 100 150 200 250 300 350 400 450 500 Thousands of words in heap (log scale) SLAM Ideal Memory 101 102 103 104 0 50 100 150 200 250 300 35…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. 2020. Reactive Probabilistic Pro- gramming. In PLDI. ACM

    work page 2020

  2. [2]

    Edwards, Nicolas Halb- wachs, Paul Le Guernic, and Robert de Simone

    Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halb- wachs, Paul Le Guernic, and Robert de Simone. 2003. The synchronous languages 12 years later. Proc. IEEE 91, 1 (2003), 64–83

    work page 2003

  3. [3]

    Keni Bernardin and Rainer Stiefelhagen. 2008. Evaluating Multiple Object Tracking Performance: The CLEAR MOT Metrics. EURASIP J. Image and Video Processing 2008 (2008)

    work page 2008

  4. [4]

    Gérard Berry. 1989. Real Time Programming: Special Purpose or General Purpose Languages. In IFIP Congress. North-Holland/IFIP, 11– 17

    work page 1989

  5. [5]

    Dariusz Biernacki, Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. 2008. Clock-directed modular code generation for synchronous data-flow languages. In LCTES. ACM, 121–130

    work page 2008

  6. [6]

    Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A

    Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. J. Mach. Learn. Res. 20 (2019), 28:1–28:6

    work page 2019

  7. [7]

    Timothy Bourke and Marc Pouzet. 2013. Zélus, a Hybrid Synchronous Language. École normale supérieure. http://zelus.di.ens.fr Distribution at: zelus.di.ens.fr

    work page 2013

  8. [8]

    Timothy Bourke and Marc Pouzet. 2013. Zélus: a synchronous lan- guage with ODEs. In HSCC. ACM, 113–118

    work page 2013

Show all 46 references
  1. [9]

    Wilson, and Michael I

    Tamara Broderick, Nicholas Boyd, Andre Wibisono, Ashia C. Wilson, and Michael I. Jordan. 2013. Streaming Variational Bayes. In NIPS. 1727–1735

    2013

  2. [10]

    Bob Carpenter, Andrew Gelman, Matthew D Hoffman, Daniel Lee, Ben Goodrich, Michael Betancourt, Marcus Brubaker, Jiqiang Guo, Peter Li, and Allen Riddell. 2017. Stan: A probabilistic programming language. J. Statistical Software 76, 1 (2017), 1–37

    2017

  3. [11]

    Paul Caspi. 1992. Clocks in Dataflow Languages. Theor. Comput. Sci. 94, 1 (1992), 125–140

    1992

  4. [12]

    Paul Caspi and Marc Pouzet. 1998. A Co-iterative Characterization of Synchronous Stream Functions. In CMCS (Electronic Notes in Theoreti- cal Computer Science), Vol. 11. Elsevier, 1–21

    1998

  5. [13]

    Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. 2006. Mixing signals and modes in synchronous data-flow systems. In EMSOFT. ACM, 73–82

    2006

  6. [14]

    Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. 2017. SCADE 6: A formal language for embedded critical software development (invited paper). In TASE. IEEE Computer Society, 1–11. 14 Reactive Probabilistic Programming PLDI ’20, June 15–20, 2020, London, UK

    2017

  7. [15]

    Jean-Louis Colaço and Marc Pouzet. 2004. Type-based initialization analysis of a synchronous dataflow language.Int. J. Softw. Tools Technol. Transf. 6, 3 (2004), 245–255

    2004

  8. [16]

    Pierre Del Moral, Arnaud Doucet, and Ajay Jasra. 2006. Sequential Monte Carlo samplers. J. Royal Statistical Society: Series B (Statistical Methodology) 68, 3 (2006), 411–436

    2006

  9. [17]

    Murphy, and Stuart J

    Arnaud Doucet, Nando de Freitas, Kevin P. Murphy, and Stuart J. Rus- sell. 2000. Rao-Blackwellised Particle Filtering for Dynamic Bayesian Networks. In UAI. Morgan Kaufmann, 176–183

    2000

  10. [18]

    Daniel Fink. 1997. A Compendium of Conjugate Priors

    1997

  11. [19]

    Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In CA V (1) (Lecture Notes in Computer Science) , Vol. 9779. Springer, 62–83

    2016

  12. [20]

    Goodman and Andreas Stuhlmüller

    Noah D. Goodman and Andreas Stuhlmüller. 2014. The Design and Implementation of Probabilistic Programming Languages. http: //dippl.org Accessed April 2020

    2014

  13. [21]

    N. J. Gordon, D. J. Salmond, and A. F. M. Smith. 1993. Novel approach to nonlinear/non-Gaussian Bayesian state estimation. IEE Proceedings F - Radar and Signal Processing 140, 2, 107–113

    1993

  14. [22]

    Halbwachs, P

    N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. 1991. The Syn- chronous Dataflow Programming Language Lustre. Proc. IEEE 79, 9 (September 1991), 1305–1320

    1991

  15. [23]

    Daniel Huang, Jean-Baptiste Tristan, and Greg Morrisett. 2017. Compil- ing Markov chain Monte Carlo algorithms for probabilistic modeling. In PLDI. ACM, 111–125

    2017

  16. [24]

    Gilles Kahn. 1974. The Semantics of a Simple Language for Parallel Programming. In IFIP Congress. North-Holland, 471–475

    1974

  17. [25]

    Rudolph Emil Kalman. 1960. A New Approach to Linear Filtering and Prediction Problems. Journal of Basic Engineering 82, 1 (03 1960), 35–45

    1960

  18. [26]

    Daniel Lundén. 2017. Delayed sampling in the probabilistic program- ming language Anglican. Master’s thesis. KTH Royal Institute of Tech- nology

    2017

  19. [27]

    Daniel Lundén, David Broman, Fredrik Ronquist, and Lawrence M. Murray. 2018. Automatic Alignment of Sequential Monte Carlo Infer- ence in Higher-Order Probabilistic Programs. CoRR abs/1812.07439 (2018)

    2018 arXiv

  20. [28]

    David Lunn, David Spiegelhalter, Andrew Thomas, and Nicky Best

  21. [29]

    Thomas P. Minka. 2001. Expectation Propagation for approximate Bayesian inference. In UAI. Morgan Kaufmann, 362–369

    2001

  22. [30]

    Michael Montemerlo, Sebastian Thrun, Daphne Koller, and Ben Weg- breit. 2002. FastSLAM: A Factored Solution to the Simultaneous Local- ization and Mapping Problem. In AAAI/IAAI. AAAI Press / The MIT Press, 593–598

    2002

  23. [31]

    Murray, Daniel Lundén, Jan Kudlicka, David Broman, and Thomas B

    Lawrence M. Murray, Daniel Lundén, Jan Kudlicka, David Broman, and Thomas B. Schön. 2018. Delayed Sampling and Automatic Rao- Blackwellization of Probabilistic Programs. In AISTATS (Proceedings of Machine Learning Research), Vol. 84. PMLR, 1037–1046

    2018

  24. [32]

    Murray and Thomas B

    Lawrence M. Murray and Thomas B. Schön. 2018. Automated learning with a probabilistic programming language: Birch. Annual Reviews in Control 46 (2018), 29–43

    2018

  25. [33]

    Praveen Narayanan, Jacques Carette, Wren Romano, Chung-chieh Shan, and Robert Zinkov. 2016. Probabilistic Inference by Program Transformation in Hakaru (System Description). In FLOPS (Lecture Notes in Computer Science) , Vol. 9613. Springer, 62–79

    2016

  26. [34]

    Avi Pfeffer. 2005. Functional Specification of Probabilistic Process Models. In AAAI. AAAI Press / The MIT Press, 663–669

    2005

  27. [35]

    Avi Pfeffer. 2009. CTPPL: A Continuous Time Probabilistic Program- ming Language. In IJCAI. 1943–1950

    2009

  28. [36]

    Pascal Raymond, Yvan Roux, and Erwan Jahier. 2008. Lutin: A Lan- guage for Specifying and Executing Reactive Scenarios. EURASIP Journal of Embedded Sytems 2008 (2008)

    2008

  29. [37]

    Daniel Ritchie, Andreas Stuhlmüller, and Noah D. Goodman. 2016. C3: Lightweight Incrementalized MCMC for Probabilistic Programs using Continuations and Callsite Caching. In AISTATS (JMLR Workshop and Conference Proceedings), Vol. 51. JMLR.org, 28–37

    2016

  30. [38]

    Eduardo D Sontag. 2013. Mathematical control theory: deterministic finite dimensional systems. Vol. 6. Springer Science & Business Media

    2013

  31. [39]

    Sam Staton. 2017. Commutative Semantics for Probabilistic Program- ming. In ESOP (Lecture Notes in Computer Science), Vol. 10201. Springer, 855–879

    2017

  32. [40]

    David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank D. Wood. 2016. Design and Implementation of Probabilistic Programming Language Anglican. In IFL. ACM, 6:1–6:12

    2016

  33. [41]

    Hoffman, Rif A

    Dustin Tran, Matthew D. Hoffman, Rif A. Saurous, Eugene Brevdo, Kevin Murphy, and David M. Blei. 2017. Deep Probabilistic Program- ming. In ICLR (Poster). OpenReview.net

    2017

  34. [42]

    Russell, and Rastislav Bodík

    Yi Wu, Lei Li, Stuart J. Russell, and Rastislav Bodík. 2016. Swift: Com- piled Inference for Probabilistic Programming Languages. In IJCAI. IJCAI/AAAI Press, 3637–3645. 15 PLDI ’20, June 15–20, 2020, London, UK A ProbZelus In this section, we provide the complete definitions o...

    2016

  35. [44]

    let µ ={[e]}sγ(s) in ∫ µ(dv, ds′)δop(v ),s′(U) {[f (e)]}iγ = (⟦e⟧iγ ,γ(f _init)) {[f (e)]}sγ = λ(s1, s2).λU

    let µ2 ={[e2]}sγ(s2) in∫ µ2(dv2, ds′ 2)δ(v1,v2),(s′ 1,s′ 2)(U) {[op(e)]}iγ = {[e]}iγ {[op(e)]}sγ = λs.λU . let µ ={[e]}sγ(s) in ∫ µ(dv, ds′)δop(v ),s′(U) {[f (e)]}iγ = (⟦e⟧iγ ,γ(f _init)) {[f (e)]}sγ = λ(s1, s2).λU . letv1, s′ 1 = ⟦e⟧sγ(s1) in let µ2 =γ(f _step)(v1)(s1) in ∫ µ...

  36. [45]

    and init xk = ck and y1 = e1 and

    let µ1 = ⟦e1⟧sγ(if v2 then s0 else s1) in∫ µ(dv1, ds′ 1)δv1,(s0,s′ 1,s′ 2)(U)     e where rec init x1 = c1 and ... and init xk = ck and y1 = e1 and ... and yn = en     i γ = ©­ « (c1, . . . ,ck), ({[e1]}iγ , . . . ,{[en]}...

  37. [46]

    letγ′ 1 =γk[v1/y1] in∫ . . . let µn = ⟦en ⟧s γ′ n−1 (sn) in∫ µn(dvn, ds′n) letγ′n =γ′ n−1[vn/yn] in let µ ={[e]}s γ′n (s) in∫ µ(dv, ds′)δv,((γ′n[x1], ...,γ′n[xk]),(s′ 1, ..., s′n),s′)(U) {[sample(e)]}iγ = ⟦e⟧iγ {[sample(e)]}sγ = λs.λU . let µ, s′ = ⟦e⟧sγ(s) in ∫ T µ(dv)δv,s′(U...

    2020

  38. [2009]

    Statistics in medicine 28, 25 (2009), 3049–3067

    The BUGS project: Evolution, critique and future directions. Statistics in medicine 28, 25 (2009), 3049–3067

    2009

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.