Prefer a chat interface with context about you and your work?
A trustful monad for axiomatic reasoning with probability and nondeterminism
Abstract The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formalization in the Coq proof assistant of a monad equipped with both choices: the geometrically convex monad. This formalization has an immediate application: it …