A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

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

Type de document :

Compte-rendu et recension critique d'ouvrage

DOI :

10.1017/S0956796821000137

Titre :

A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism

Auteur(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

Titre de la revue :

Journal of Functional Programming

Éditeur :

Cambridge University Press (CUP)

Date de publication :

2021-07-15

ISSN :

0956-7968

Discipline(s) HAL :

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

Résumé en anglais : [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 ...
Lire la suite >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.Lire moins >

Langue :

Anglais

Vulgarisation :

Non

Commentaire :

28 pages, submitted

Collections :