A trustful monad for axiomatic reasoning with probability and nondeterminism

DOI10.1017/S0956796821000137zbMath1493.03004arXiv2003.09993MaRDI QIDQ5152658

Jacques Garrigue, Takafumi Saikawa, Reynald Affeldt, David E. Nowak

Publication date: 24 September 2021

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2003.09993

zbMATH Keywords

monadCoqprobabilistic choicenondeterministic choiceconvex powerset monadgeometrically convex monadmonadic equational reasoning

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Measure construction by extension in dependent type theory with application to integration ⋮ Towards a practical library for monadic equational reasoning in Coq

Uses Software

• Coq
• Irdis
• UniMath
• Idris
• GitHub
• finmap

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Semantic domains for combining probability and non-determinism
• An invitation to general algebra and universal constructions.
• Verified tail bounds for randomized programs
• A hierarchy of monadic effects for program verification using equational reasoning
• Formal adventures in convex and conical spaces
• Formalization of Shannon's theorems
• Postulates for the barycentric calculus
• Weakest Precondition Reasoning for Expected Run–Times of Probabilistic Programs
• Experience Implementing a Performant Category-Theory Library in Coq
• Convexity, Duality and Effects
• Packaging Mathematical Structures
• Unifying Theories of Programming with Monads
• Abstraction, Refinement and Proof for Probabilistic Systems
• Combining probabilistic and non-deterministic choice via weak distributive laws
• Just do it
• Probabilistic Completion of Nondeterministic Models
• Canonical Structures for the Working Coq User
• Category Theory in Coq 8.5
• Idris, a general-purpose dependently typed programming language: Design and implementation
• Distributing probability over non-determinism

This page was built for publication: A trustful monad for axiomatic reasoning with probability and nondeterminism