English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Tools annual

Global: Zendy Free Plan

Global: Zendy Tools monthly

Global: Zendy Plus monthly

The algebraic properties of the combination of probabilistic choice andnondeterministic choice have long been a research topic in program semantics.This paper explains a formalization in the Coq proof assistant of a monadequipped with both choices: the geometrically convex monad. This formalizationhas an immediate application: it provides a model for a monad that implements anon-trivial interface which allows for proofs by equational reasoning usingprobabilistic and nondeterministic effects. We explain the technical choices wemade to go from the literature to a complete Coq formalization, from which weidentify reusable theories about mathematical structures such as convex spacesand concrete categories, and that we integrate in a framework for monadicequational reasoning.

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism