Semantics of probabilistic programs

1981/06/01 by Dexter Kozen · 508 citations
Computer Science · Mathematics · #Artificial intelligence #Computer science #Denotational semantics #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Operational semantics #Probabilistic logic #Programming language #Semantics (computer science) #Space (punctuation) #Theoretical computer science

paper · pdf · doi:10.1016/0022-0000(81)90036-2

published in Journal of Computer and System Sciences 22(3), 328-350 (Elsevier BV)

openalex publication_date 1981/06/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/02

Cited by

• A probabilistic PDL
• DynamicPPL: Stan-like Speed for Dynamic Probabilistic Models
• Reasoning about Recursive Probabilistic Programs
• Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata
• Relatively Complete Verification of Probabilistic Programs
• Conditioning in Probabilistic Programming
• RankPL: A Qualitative Probabilistic Programming Language
• Verification Logics for Quantum Programs
• Formal Semantics of a Classical-Quantum Language
• On the Hardness of Almost-Sure Termination
• Quantum Domain Theory - Definitions and Applications
• Large Language Models as Nondeterministic Causal Models
• Results on the quantitative mu-calculus qMu
• Weighted Automata for Exact Inference in Discrete Probabilistic Programs
• Parallelizable Feynman-Kac Models for Universal Probabilistic Programming
• A Theory of Slicing for Probabilistic Control-Flow Graphs
• Verifying Sampling Algorithms via Distributional Invariants
• Healthiness from Duality
• Static Factorisation of Probabilistic Programs With User-Labelled Sample Statements and While Loops
• To Zip Through the Cost Analysis of Probabilistic Programs
• A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design
• Raising Expectations: Automating Expected Cost Analysis with Types
• Proving Almost-Sure Termination of Probabilistic Programs via Incremental Pruning
• An Adequate While-Language for Stochastic Hybrid Computation
• Quantifying Program Bias
• Effectuses in Categorical Quantum Foundations
• Alternation in Quantum Programming: From Superposition of Data to Superposition of Programs
• Conditioning in Probabilistic Programming
• Sound Probabilistic Inference via Guide Types
• On Measure Quantifiers in First-Order Arithmetic (Long Version)
• Central Moment Analysis for Cost Accumulators in Probabilistic Programs
• Forward and Backward Simulations for Partially Observable Probability
• Counterexample-Guided Polynomial Loop Invariant Generation by Lagrange Interpolation
• ε-Distance via Lévy-Prokhorov Lifting
• Compositional semantics for new paradigms: probabilistic, hybrid and beyond
• Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments
• Expected-Cost Analysis for Probabilistic Programs and Semantics-Level Adaption of Optional Stopping Theorems
• Safety, Relative Tightness and the Probabilistic Frame Rule
• Homotopical Observables and the Langlands Program via ∞-Topoi
• Towards Verified Stochastic Variational Inference for Probabilistic Programs
• Tensor Probabilistic Model Checking of Finite-Horizon Markov Chains
• Extensional Denotational Semantics of Higher-Order Probabilistic Programs, Beyond the Discrete Case
• Computable Exchangeable Sequences Have Computable de Finetti Measures
• Exact Evaluation of Probabilistic Programs with Cylindrical Algebraic Decomposition
• Confluence in Probabilistic Rewriting
• Continuity spaces: Reconciling domains and metric spaces
• Proof rules for purely quantum programs
• Analyzing Decoders for Quantum Error Correction
• Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming
• A Cost-Aware Probability Monad for Liquid Haskell
• Domains of commutative C*-subalgebras
• Coinductive Proof Principles for Stochastic Processes
• Supermartingales for Unique Fixed Points: A Unified Approach to Lower Bound Verification
• Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes [europepmc]
• Automated Termination Analysis of Polynomial Probabilistic Programs [europepmc]