Séminaire Cambium, Inria Paris, 2 rue Simone Iff
                            Salle A215, bâtiment A
                           Lundi 5 décembre, 10h30

                                Nicolas Chappe
                               ENS de Lyon, LIP

                                Choice Trees:
     Representing Nondeterministic, Recursive, and Impure Programs in Coq

We introduce Choice Trees (ctrees), a monad for modeling nondeterministic,
recursive, and impure programs in Coq. Inspired by Xia et al’s itrees, this
novel data structure embeds computations into coinductive trees with three
kind of nodes: external events, and two variants of nondeterministic
branching. This apparent redundancy allows us to provide shallow embedding of
denotational models with internal choice in the style of ccs, while recovering
an inductive LTS view of the computation. Ctrees inherit a vast collection of
bisimulation and refinement tools, with respect to which we establish a rich
equational theory.

We connect ctrees to the itrees infrastructure by showing how a monad morphism
embedding the former into the latter permits to use ctrees to implement
nondeterministic effects. We demonstrate the utility of ctrees by using them
to model concurrency semantics in two case studies: ccs and cooperative
multithreading.

This work is implemented as a Coq library publicly available at:
https://github.com/vellvm/ctrees/tree/popl23

The preprint of the accompanying paper is available at:
https://perso.ens-lyon.fr/yannick.zakowski/papers/ctrees.pdf

            Vous pouvez vous abonner à nos annonces de séminaires:
                     http://cambium.inria.fr/seminar.html

             Nos séminaires sont accessibles en ligne en direct:
                  https://webconf.math.cnrs.fr/b/fra-ryy-fjn