Healthiness conditions for predicate transformers

DOI10.1016/j.entcs.2015.12.016zbMath1351.68076OpenAlexW2212044066WikidataQ113317725 ScholiaQ113317725MaRDI QIDQ5971403

Klaus Keimel

Publication date: 16 December 2016

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2015.12.016

zbMATH Keywords

predicate transformerscommuting operationsentropic algebrashealthiness conditionscontinuation monad

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantic domains for combining probability and non-determinism
• Extending algebraic operations to D-completions
• Relating direct and predicate transformer partial correctness semantics for an imperative probabilistic-nondeterministic language
• Notions of computation and monads
• Generic weakest precondition semantics from monads enriched with order
• A Minkowski type duality mediating between state and predicate transformer semantics for a probabilistic nondeterministic language
• Semantics of probabilistic programs
• Separable modes
• Completeness of continuation models for \(\lambda_\mu\)-calculus
• A Convenient Category of Domains
• Commutative monads as a theory of distributions
• Predicate transformers for extended probability and non-determinism
• Abstraction, Refinement and Proof for Probabilistic Systems
• Continuous Lattices and Domains
• Prevision Domains and Convex Powercones
• Quantum weakest preconditions

This page was built for publication: Healthiness conditions for predicate transformers