Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
From MaRDI portal
Publication:541217
DOI10.1016/J.TCS.2010.12.029zbMath1226.68040OpenAlexW2013333738MaRDI QIDQ541217
A. Rosenbusch, Klaus Keimel, Thomas Streicher
Publication date: 6 June 2011
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2010.12.029
denotational semanticspredicate transformersMinkowski dualityprobabilistic-nondeterministic computationweakest liberal precondition
Related Items (3)
The expectation monad in quantum foundations ⋮ Generic weakest precondition semantics from monads enriched with order ⋮ Healthiness conditions for predicate transformers
Cites Work
- Unnamed Item
- Semantic domains for combining probability and non-determinism
- A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language
- Domain-Theoretic Foundations of Functional Programming
- Predicate transformers for extended probability and non-determinism
- Abstraction, Refinement and Proof for Probabilistic Systems
- Continuous Lattices and Domains
- Partial correctness for probabilistic demonic programs
This page was built for publication: Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language