Semantics of probabilistic programs

By Dexter Campbell Kozen. 1979

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Proving Differential Privacy via Probabilistic Couplings (2016, neutral): “The semantics of programs is standard [4, 22].”
Formal certification of code-based cryptographic proofs (2009, methodology): “[22] D.Kozen.”
PSI: Exact Symbolic Inference for Probabilistic Programs (2016, background): “Denotational semantics for the source language is easy to define by extending [30], but defining the measure semantics for distribution expressions is more challenging.”
Probabilistic programming (2014, background): “Though the idea has been around since the 80’s [34, 56], in the past decade there has been a lot of progress in building model checkers such as PRISM [36] and MRMC [29].”
Reasoning about Probabilities in Unbounded First-Order Dynamical Domains (2017, methodology): “The Fagin-Halpern scheme shares some similarity with probabilistic logics for programs [Kozen, 1981] and variants thereof [Halpern and Tuttle, 1993; Van Benthem et al.”
Coupling proofs are probabilistic product programs (2016, methodology): “The denotational semantics of programs is adapted from the seminal work of Kozen [36].”
Measure Transformer Semantics for Bayesian Machine Learning (2011, background): “Kozen [17] develops a probabilistic semantics for while-programs augmented with random assignment.”
A Program Logic for Union Bounds (2016, unknown): “Kozen’s seminal paper [28] studies two semantics for a core probabilistic imperative language.”
Proving differential privacy with shadow execution (2019, background): “, [8, 42]), we assume a subdistribution instead of a distribution, since sub-distribution gives rise to an elegant program semantics in face of non-terminating programs [28].”
A First-Order Logic of Probability and Only Knowing in Unbounded Domains (2016, methodology): “The Fagin-Halpern scheme shares some similarity with probabilistic logics for programs (Kozen 1981) and variants thereof (Halpern and Tuttle 1993; Van Benthem, Gerbrandy, and Kooi 2009); see (Fagin and Halpern 1994) for discussions.”
Compiling Stan to generative probabilistic languages and extension to deep probabilistic programming (2021, background): “While the semantics of probabilistic languages have been extensively studied [14, 15, 18, 30], to the best of our knowledge little is known about the relationship between Stan and generative PPLs.”
LightDP: towards automating differential privacy proofs (2016, methodology): “…be mitigated if the algorithms used to manipulate the data, answer queries, and build statistical models satisfy differential privacy (Dwork et al. 2006b) — a set of restrictions on their probabilistic behavior that provably limit the ability of attackers to infer individual-level sensitive…”
A lambda-calculus foundation for universal probabilistic programming (2015, methodology): “In deﬁning the ﬁrst semantics of the calculus, we use the classical observation (Kozen 1979) that a probabilistic program can be interpreted as a deterministic program parametrized by the sequence of random draws made during the evaluation.”
AutoPriv: Automating Differential Privacy Proofs (2016, methodology): “Notice that we do not require a∈A µ a = 1, a special case when µ is a distribution, since sub-distribution gives rise to an elegant semantics for programs that may not terminate (Kozen 1981).”
Approximate Computing: A Survey (2016, background): “In 1979, Kozen recognized the need for both a syntax and semantics for programs that use randomness during execution [30].”