Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq
This paper introduces 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 itree 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.
Fri 20 JanDisplayed time zone: Eastern Time (US & Canada) change
10:45 - 12:00
|Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice|
|Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq|
Nicolas Chappe University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Paul He University of Pennsylvania, Ludovic Henrio University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Yannick Zakowski University of Lyon - ENS Lyon - UCBL - CNRS - Inria - LIP, Steve Zdancewic University of PennsylvaniaDOI
|Hefty Algebras: Modular Elaboration of Higher-Order Algebraic EffectsRecorded|