Semantics of probabilistic programs

DOI10.1016/0022-0000(81)90036-2zbMATH Open0476.68019OpenAlexW2024355065MaRDI QIDQ1159979FDOQ1159979

Authors: Dexter Kozen 

Publication date: 1981

Published in: Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0022-0000(81)90036-2

zbMATH Keywords

ordered domainsaction on fixed inputsprograms as continuous linear operators on a Banach space of measuresprograms as partial measurable functions on a measurable spacesemantics for a high level probabilistic programming language

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Specification and verification (program logics, model checking, etc.) (68Q60)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Einige abstrakte Begriffe in der numerischen Mathematik (Anwendungen der Halbordnung).(Some abstract notions in the numerical mathematic. (Applications et semiorder))
• A Fast Monte-Carlo Test for Primality
• A Powerdomain Construction
• Title not available (Why is that?)
• Expected time bounds for selection
• Title not available (Why is that?)
• Title not available (Why is that?)
• Formal models for some features of programming languages
• Title not available (Why is that?)

Cited In (89)

• Reversible monadic computing
• Inferring expected runtimes of probabilistic integer programs using expected sizes
• Learning probabilistic termination proofs
• Model checking finite-horizon Markov chains with probabilistic inference
• Semantics of probabilistic programs: a weak limit approach
• On higher-order probabilistic subrecursion
• On higher-order probabilistic subrecursion
• A computable approach to measure and integration theory
• On the hardness of almost-sure termination
• Weakest precondition reasoning for expected run-times of probabilistic programs
• Dynamic logic with program specifications and its relational proof system
• Partial correctness for probabilistic demonic programs
• Stochastic differential dynamic logic for stochastic hybrid programs
• Reasoning about probabilistic sequential programs
• Correctness of sequential Monte Carlo inference for probabilistic programming languages
• Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
• On the hardness of analyzing probabilistic programs
• An application of computable distributions to the semantics of probabilistic programming languages
• Commutative semantics for probabilistic programming
• Understanding probabilistic programs
• On Lexicographic Proof Rules for Probabilistic Termination
• The probabilistic powerdomain for stably compact spaces
• Approximating labelled Markov processes
• Commutativity of quantum weakest preconditions
• A probabilistic dynamic logic
• Decidability of finite probabilistic propositional dynamic logics
• Hennessy-Milner results for probabilistic PDL
• Borel kernels and their approximation, categorically
• Unifying theories of programming with monads
• Quantification of integrity
• A type theory for probabilistic and Bayesian reasoning
• Probabilistic NetKAT
• Probabilistic analysis of programs: a weak limit approach
• A probabilistic PDL
• Continuity spaces: Reconciling domains and metric spaces
• Automated termination analysis of polynomial probabilistic programs
• A generalisation of stationary distributions, and probabilistic program algebra
• The converse of a stochastic relation
• Continualization of probabilistic programs with correction
• The expectation monad in quantum foundations
• On finite-state approximants for probabilistic computation tree logic
• Categories of timed stochastic relations
• Probabilistic logics based on Riesz spaces
• Generic weakest precondition semantics from monads enriched with order
• An effect-theoretic account of Lebesgue integration
• \(\mathcal{MOQA}\); unlocking the potential of compositional static average-case analysis
• Bisimulation for labelled Markov processes
• Proofs of randomized algorithms in Coq
• Confluence in probabilistic rewriting
• Rigorous roundoff error analysis of probabilistic floating-point computations
• Probabilistic abstract interpretation of imperative programs using truncated normal distributions
• A probability perspective
• VPHL: a verified partial-correctness logic for probabilistic programs
• From probability monads to commutative effectuses
• Approximate counting in SMT and value estimation for probabilistic programs
• A denotational semantics for low-level probabilistic programs with nondeterminism
• Formal semantics of a classical-quantum language
• Moment-based analysis of Bayesian network properties
• The Hennessy-Milner equivalence for continuous time stochastic logic with mu-operator
• The beta-Bernoulli process and algebraic effects
• Measure and probability for concurrency theorists
• Computable exchangeable sequences have computable de Finetti measures
• Probabilistic rely-guarantee calculus
• Data-Driven Invariant Learning for Probabilistic Programs
• Labelled Markov processes as generalised stochastic relations
• Conditioning in probabilistic programming
• Characterizations of semantic domains for randomized algorithms
• Healthiness conditions for predicate transformers
• Towards logical foundations for probabilistic computation
• Title not available (Why is that?)
• Linear Structures for Concurrency in Probabilistic Programming Languages
• Control-data separation and logical condition propagation for efficient inference on probabilistic programs
• Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs
• A theory of slicing for probabilistic control flow graphs
• Title not available (Why is that?)
• The syntactic side of autonomous categories enriched over generalised metric spaces
• On lexicographic proof rules for probabilistic termination
• Multisets and distributions, in drawing and learning
• Structure in machine learning
• Mixed nondeterministic-probabilistic automata: blending graphical probabilistic models with nondeterminism
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Automated Expected Amortised Cost Analysis of Probabilistic Data Structures
• Does a Program Yield the Right Distribution?
• Curry and Howard meet Borel
• Automatic alignment in higher-order probabilistic programming languages
• On probabilistic techniques for data flow analysis
• Probabilistic logic over paths
• Generative Datalog with continuous distributions
• Measure transformer semantics for Bayesian machine learning

This page was built for publication: Semantics of probabilistic programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1159979)