A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi

Document type :

Compte-rendu et recension critique d'ouvrage

DOI :

10.1017/S0956796821000137

Title :

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

Author(s) :

Affeldt, Reynald [Auteur]
National Institute of Advanced Industrial Science and Technology [AIST]
Garrigue, Jacques [Auteur]
Nagoya University
Nowak, David [Auteur]

Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Saikawa, Takafumi [Auteur]
Nagoya University

Journal title :

Journal of Functional Programming

Publisher :

Cambridge University Press (CUP)

Publication date :

2021-07-15

ISSN :

0956-7968

HAL domain(s) :

Informatique [cs]/Logique en informatique [cs.LO]

English abstract : [en]

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 ...
Show more >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 provides a model for a monad that implements a non-trivial interface which allows for proofs by equational reasoning using probabilistic and nondeterministic effects. We explain the technical choices we made to go from the literature to a complete Coq formalization, from which we identify reusable theories about mathematical structures such as convex spaces and concrete categories, and that we integrate in a framework for monadic equational reasoning.Show less >

Language :

Anglais

Popular science :

Non

Comment :

28 pages, submitted

Collections :