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

Nicolas Chappe

Univ Lyon, EnsL, UCBL, CNRS, Inria,  LIP, F-69342, LYON Cedex 07

Paul He

University of Pennsylvania

Ludovic Henrio

Univ Lyon, EnsL, UCBL, CNRS, Inria,  LIP, F-69342, LYON Cedex 07

Yannick Zakowski

Univ Lyon, EnsL, UCBL, CNRS, Inria,  LIP, F-69342, LYON Cedex 07

Steve Zdancewic

University of Pennsylvania

This paper introduces Choice Trees (), a monad for modeling nondeterministic, recursive, and
impure programs in .
Inspired by 's , 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 , while
recovering an inductive LTS view of the computation.
inherit a vast collection of bisimulation and refinement tools, with respect to
which we establish a rich equational theory.

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

<concept_desc>Computer systems organization Embedded systems</concept_desc>
<concept_desc>Computer systems organization Redundancy</concept_desc>
<concept_desc>Computer systems organization Robotics</concept_desc>
<concept_desc>Networks Network reliability</concept_desc>

§ INTRODUCTION

Reasoning about and modeling nondeterministic computations is important for many
purposes. Formal specifications use nondeterminism to abstract away from the
details of implementation choices.  Accounting for nondeterminism is crucial
when reasoning about the semantics of concurrent and distributed systems, which
are, by nature, nondeterministic due to races between threads, locks, or message
deliveries.  Consequently, precisely defining nondeterministic behaviors and
developing the mathematical tools to work with those definitions has been an
important research endeavor, and has led to the development of
formalisms like nondeterministic automata, labeled transition systems
and relational operational semantics <cit.>, powerdomains <cit.>, or
game semantics <cit.>, among others, all of which have been used to give semantics to
nondeterministic programming language features such as
concurrency <cit.>.

In this paper, we are interested in developing tools for modeling
nondeterministic computations in a dependent type theory such as Coq's
CIC <cit.>.  Although any of the formalisms mentioned above could be used
for such purposes (and many have been <cit.>), those
techniques offer various tradeoffs when it comes to the needs of formalization:
automata, and labeled transitions systems, while offering powerful
bisimulation proof principles, are not easily made modular (except, perhaps, with complex extensions to the framework <cit.>).  Relationally-defined operational semantics are flexible and
expressive, but again suffer from issues of compositionality, which
makes it challenging to build general-purpose libraries
that support constructing complex models.  Conversely, powerdomains and game
semantics are more denotational approaches, aiming to ensure compositionality
by construction; however, the mathematical structures involved are themselves
very complex, typically involving many relations and constraints <cit.> that are not easy to implement in constructive logic (though there are some notable exceptions <cit.>).
Moreover, in all of the above-mentioned approaches, there are other tensions at
play. For instance, how “deep” the embedding is affects the amount of effort
needed to implement a formal semantics—“shallower” embeddings typically
allow more re-use of metalanguage features, e.g., meta-level function
application can obviate the need to define and prove properties about a
substitution operation; “deeper” embeddings can side-step meta-level
limitations (such as Coq's insistence on pure, total functions) at the cost of
additional work to define the semantics.  Moreover, these tradeoffs can
have significant impact on how difficult it is to use other tools and
methodologies: for instance, to use QuickChick <cit.>, one must be able to extract an
executable interpreter from the semantics, something that isn't always easy or

This paper introduces a new formalism designed specifically to facilitate the
definition of and reasoning about nondeterministic computations in Coq's
dependent type theory.  The key idea is to update Xia, et al.'s interaction trees ()
framework <cit.> with native support for nondeterminisic “choice
nodes” that represent internal choices made during computation. The
main technical contributions of this paper are to introduce the definition of
these  (“choice trees”) and to develop the suitable metatheory and equational reasoning principles to accommodate that change.

We believe that  offer an appealing, and novel, point in the design
space of formalisms for working with nondeterministic specifications within type
theory.  Unlike purely relational specifications, build nondeterminism
explicitly into a datatype, as nodes in a tree, and the nondeterminism is
realized propositionally at the level of the equational theory, which determines
when two  computations are in bisimulation.  This means that the user
of  has more control over how to represent nondeterminism and when to apply the
incumbent propositional reasoning. By reifying the choice construct into a
data structure, one can write meta-level functions that manipulate ,
rather than working entirely within a relation on syntax.  This design allows us
to bring to bear the machinery of monadic interpreters to refine the
nondeterminism into an (executable) implementation.

can represent such choice nodes, in our experience, using that feature to model
“internal” nondeterminism is awkward: the natural equational theory for
is too fine, and other techniques, such as interpretation into
Prop, don't work out neatly.

At the same time, the notion of bisimulation for  is still connected
to familiar definitions like those from labeled transition systems (), meaning
that much of the well-developed theory from prior work can be imported whole-sale.
Indeed, we define bisimilarity for  by viewing them as LTSs and
applying standard definitions.  The fact that the definition of bisimulation
ends up being subtle and nontrivial is a sign that we gain something by working
with the : like their  predecessors,  have
compositional reasoning principles, the type is a monad, and the useful
combinators for working with , namely sequential composition,
iteration and recursion, interpretation, etc., all carry over directly.

, though, further allow us to
conveniently, and flexibly, define nondeterminstic semantics, ranging from
simple choice operators to various flavors of parallel composition.  The benefit
is that, rather than just working with a “raw” LTS directly, we can construct
one using the  combinators—this is a big benefit because, in
practice, the LTS defining the intended semantics of a nondeterministic
programming language cannot easily be built in a compositional way without using some kind of intermediate representation, which is exactly what provides (see the discussion
about Figure <ref>).  A key technical novelty of our
definition is that it makes a distinction between stepping choices (which correspond to $\tau$ transitions and introduce new LTS states) and delayed choices (which don't correspond to a transition and don't create a state in the LTS). This design allows for compositional
construction of the LTS and generic reasoning rules that are usable in any

The net result of our contributions is a library, entirely formalized in Coq,
that  offers flexible building blocks for constructing nondeterministic, and
hence concurrent, models of computation.  To demonstrate the applicability of this library, we
use it to implement the semantics from two different formalisms:  <cit.> and a language with
cooperative threads inspired from the literature <cit.>.  Crucially, in both of these scenarios, we are
able to define the appropriate parallel composition combinators such
that the semantics of the programming language can be defined fully
compositionally (i.e., by straightforward induction on the syntax).  Moreover, we
recover the classic definition of program equivalence for directly from the
equational theory induced by the encoding of the semantics using ; for the language with cooperative threading, we prove some standard program equivalences.

To summarize, this paper makes the following contributions:

* We introduce , a novel data structure for defining
nondeterministic computations in type theory, along with a set of combinators
for building semantic objects using .

* We develop the appropriate metatheory needed to reason about strong and
weak bisimilarity of , connecting their semantics to concepts
familiar from labeled transition systems.

* We show that  admit appropriate notions of refinement and that
we can use them to construct monadic interpreters; we show that  can
be faithfully embedded into .

* We demonstrate how to use  in two case studies: (1) to define a
semantics for Milner's classic and prove that the resulting derived
equational theory coincides with the one given by the standard operational
semantics, and (2) to model cooperative multithreading with support for
and operations and prove nontrivial program equivalences.

All of our results have been implemented in , and all claims in this paper
are fully mechanically verified.
For expository purposes, we stray away from 's syntax in the body of this
paper, but systematically link our claims to their formal counterpart via
hyperlinks represented as ().

The remainder of the paper is organized as follows. The next section gives some
background about interaction trees and monadic interpreters, along with a
discussion of the challenges of modeling nondeterminism, laying the foundation
for our results. We introduce the  data structure and its main
combinators in Section <ref>. Section <ref> introduces
several notions of equivalences over —(coinductive) equality, strong
bisimilarity, weak bisimilarity, and trace equivalence—and describes its core
equational theory. Section <ref> describes how to interpret
uninterpreted events in an into “choice” branches in a , as
well as how to define the monadic interpretation of events from .
Section <ref> describes our first case study, a model for .
Section <ref> describes our second case study, a model for the language extended with cooperative multithreading. Finally, Section <ref>
discusses related work and concludes.

§ BACKGROUND

§.§ Interaction trees and monadic interpreters

Monadic interpreters have grown to be an attractive way to mechanize the
semantics of a wide class of computational systems in dependent typed theory,
such as the one found in many proof assistants, for which the host language is
purely functional and total.  In the Coq ecosystem, interaction
trees <cit.> provide a rich library for building and reasoning about
such monadic interpreters.  By building upon the free(r)
monad <cit.>, one can both design highly reusable components, as
well as define modular models of programming languages more amenable to
evolution.  By modeling recursion coinductively, in the style of Capretta's
delay monad <cit.>, such interpreters can model non-total object
languages while retaining the ability to extract correct-by-construction,
executable, reference interpreters.  By generically lifting monadic
implementations of effects into a monad homomorphism, complex interpreters can
be built by stages, starting from an initial structure where all effects are
free and incrementally introducing their implementation.  Working in a proof
assistant, these structures are well suited for reasoning about program
equivalence and program refinement: each monadic structure comes with its own
notion of refinement, and the layered infrastructure gives rise to increasingly
richer equivalences <cit.>, starting from the free monad, which comes
with no associated algebra.

CoInductive itree (E: Type -> Type) (R: Type) : Type :=
| Ret (r: R)                                  (* computation terminating with value r *)
| Vis A: Type (e : E A) (k : A -> itree E R) (* event e yielding an answer in A *)
| later (t: itree E R).                       (* "silent" tau transition with child t *)

Interaction trees: definition

Interaction trees are coinductive data structures for representing (potentially
divergent) computations that interact with an external environment through
visible events.  A definition of the datatype is shown in
Figure <ref>.[The signature of is presented with
a positive coinductive datatype for expository purposes. The actual
implementation is defined in the negative style.]  The datatype takes as its
first parameter a signature—described as a family of types E : Type ->
Type—that specifies the set of interactions the computation may have with
the environment.  The Vis constructor builds a node in the tree
representing such an interaction, followed by a continuation indexed by the
return type of the event.  The second parameter, R, is the result
type, the type of values that the entire computation may return, if it halts. The
constructor Ret builds such a pure computation, represented as a leaf.
Finally, the constructor models an internal, non-observable step of
computation, allowing the representation of silently diverging computations; it
is also used for guarding corecursive definitions.[The library
uses Tau to represent nodes.  Tau and $\tau$ are overloaded
in our context, so we rename it to here to avoid ambiguity. will replace the (i.e. Tau) constructor with a more general
construct anyway.]

To illustrate the approach supported by , and motivate the contributions
of this paper, we consider how to define the semantics for a simple imperative programming language, :

xe c1c2 bc

The language contains a construct, assignments, sequential composition, and loops—we
assume a simple language of expressions, $e$, that we omit here.
Consider the following programs:

p_1  p_2 x0xy p_3 xy

Following a semantic model for built on in the style of
<cit.>, one builds a semantics in two stages. First,
commands are represented as monadic computations of type itree MemE unit:
commands do not return values, so the return type of the computation is
the trivial unit type; interactions with the memory are (at first) left
uninterpreted, as indicated by the event signature MemE.
This signature encodes two operations:  rd yields a
value, while  wr yields only the acknowledgment that the operation took
place, which we encode again using unit.

Variant MemE : Type -> Type :=
| rd (x : var)                : MemE value
| wr (x : var) (v : value) : MemE unit

Indexing by the value type in the continuation of rd events
gives rise to non-unary branches in the tree representing these programs. For
instance, the programs $p_1,p_2,p_3$ are, respectively, modeled at this stage by
the trees shown in Figure <ref>. These diagrams omit the Vis and
Ret constructors, because their presence is clear from the picture. For
example, the second tree would be written  as

\[p_2 = \ilc{Vis (wr x 0) (fun _ => Vis (rd y) (fun ans => (Vis (wr x ans) (fun _ => Ret tt))))}.\]

\[
\begin{array}{ccc}
\multicolumn{3}{l}{\sem{\cwhile{\true}{\cskip}} \qquad \quad \sem{\cseq{\cassign{x}{0}}{\cassign{x}{y}}} \hspace{1.4in} \sem{\cassign{x}{y}} } \\
\qquad \quad
\begin{forest}
% for tree={circle, l=0.3cm, l sep=0.3cm, s sep = 5pt}
[\delay, name=foo
\draw[dotted] (foo) --+(0,-1);
\end{forest}}
\begin{forest}
% for tree={circle, , l sep=0.3cm, s sep = 5pt}
[\tm{wr~x~0}[tt]] [\tm{wr~x~1}[tt]] [\dots] [\tm{wr~x~n}[tt]] [\dots]
\end{forest}}
\begin{forest}
% for tree={circle, , l sep=0.3cm, s sep = 5pt}
[\tm{wr~x~0}[tt]] [\tm{wr~x~1}[tt]] [\dots] [\tm{wr~x~n}[tt]] [\dots]
\end{forest}}
\end{array}
\]

Example denoting the programs $p_1$, $p_2$, and $p_3$.

The nodes in the first tree are the guards from
Capretta's monad: because the computation diverges silently, it is modeled as
an infinite sequence of such guards. The equivalence used for
computations in the monad is a weak bisimulation, dubbed
equivalence up-to taus (), which allows one to ignore finite sequences of
nodes when comparing two trees. It remains termination-sensitive: the silently diverging
computation is not equivalent to any other .

With , no assumptions about the semantics of the uninterpreted memory
events is made.  Although one would expect $p_2$ and $p_3$ to be equivalent
as programs, their trees are not since the former starts with a different
event than the latter.  This missing algebraic equivalence is concretely
recovered at the second stage of modeling: programs are given a semantics
by interpreting the trees into the state monad, by handling the
MemE events.  This yields computations in stateT mem (itree voidE)
unit, or, unfolding the definition, mem -> itree voidE (mem * unit).  Here, voidE is the
“empty” event signature, such that an at that type either silently diverges
or deterministically returns an answer.  For $p_2$ and $p_3$, assuming an initial state
m, the computations become (writing the trees horizontally to save space):

\[
\begin{array}{lcl}
\ilc{interp}\ h_{mem}\ \sem{p_2} ~\ilc{m} &=&
\delay - \delay - \delay - (\ilc{m}\{x\gets 0\}\{x\gets \ilc{m}(y)\}, tt)
\\
\ilc{interp}\ h_{mem}\ \sem{p_3}~ \ilc{m} &=&
\delay - \delay - (\ilc{m}\{x\gets \ilc{m}(y)\}, tt)
\end{array}
\]

The nodes are introduced by the interpretation of the memory events. More precisely,  an interp combinator  applies
the handler $h_{mem}$ to the rd and wr nodes of the trees, implementing their
semantics in terms of the state monad.  Assuming an appropriate implementation
of the memory, one can show that \(\ilc{m}\{x\gets0\}\{x\gets \ilc{m}(y)\}\) and
\(\ilc{m}\{x\gets \ilc{m}(y)\}\) are extensionally equal, and hence $p_2$ and
$p_3$ are eutt after interpretation.

§.§ Nondeterminism

While the story above is clean and satisfying for stateful effects,
nondeterminism is much more challenging.  Suppose we extend with a
branching operator pq whose semantics is to nondeterministically pick a
branch to execute. This new feature is modeled very naturally using a
boolean-indexed event, creating a binary branch in the tree.  The new event
signature, a sample use, and the corresponding tree are shown below:

Variant Flip : Type -> Type :=
| flip : Flip bool.

Vis flip (fun b => if b then p else q)

Naturally, as with memory events, does not come with its expected algebra:
associativity, commutativity and idempotence.
To recover these necessary equations to establish program equivalences
such as $p_3 \equiv \cbr{p_2}{p_3},$ we need to find a suitable
monad to interpret into.

used this approach in the Vellvm project
<cit.> for formalizing the nondeterministic features of the .
Their model consists of a propositionally-specified set of computations:
ignoring other effects, the monad they use is itree E _ -> Prop.
The equivalence they build on top of it essentially amounts to a form of
bijection up-to equivalence of the contained monadic computations.
However, this approach suffers from several drawbacks.
First, one of the monadic laws is broken: the bind operation does not associate to the left.
Although stressed in the context of Vellvm <cit.> and Yoon et al.'s work on layered
monadic interpreters <cit.>,
this issue is not specific to but rather to an hypothetical “Prop Monad Transformer”,
i.e. to "fun M X => M X -> Prop", as pointed out previously in <cit.>.
The definition is furthermore particularly difficult to work with. Indeed, the corresponding monadic
equivalence is a form of bijection up-to setoid: for any trace in the source, we must existentially exhibit
a suitable trace in the target. The inductive nature of this existential is problematic: one usually cannot exhibit
upfront a coinductive object as witness, they should be produced coinductively.

Second, the approach is very much akin to identifying a communicating system with
its set of traces, except using a richer structure, namely monadic computations,
instead of traces: it forgets all information about when nondeterministic choices are made.
As has been well identified by the process calculi tradition, and while trace equivalence is sometimes the
desired relation, such a model leads
to equivalences of programs that are too coarse to be compositional in general.
In a general purpose semantics library, we believe we should strive to provide as much compositional reasoning as possible and thus our tools  support both trace equivalence, and bisimulations <cit.>.
Third, because the set of computations is captured propositionally,

this interpretation is incompatible with the generation of an executable interpreter by extraction, losing
one of the major strengths of  the framework.
work around this difficulty by providing two
interpretations of their nondeterministic events, and formally relating them.
But this comes at a cost — the promise of a sound interpreter for free is broken — and with constraints —
non-determinism must come last in the stack of interpretations, and combinators whose equational theory is sensible
to nondeterminism are essentially impossible to define.

This difficulty with properly tackling nondeterminism extends also to
concurrency.   used to prove
the linearizability of concurrent objects <cit.>. Here too, they rely on sets of
linearized traces and consider their interleavings. While a reasonable
solution in their context, that approach strays from the monadic interpreter style
and fails to capture bisimilarity.

This paper introduces , a suitable monad for modeling nondeterministic
effects. As with , the structure is compatible with divergence, external
interaction through uninterpreted events, extraction to executable reference
interpreters, and monadic interpretation.  The core intuition is based on the
observation that the tree-like structure from is indeed the right one
for modeling nondeterminism. The problem arises from how the definition
of observes which branch is taken, requiring that all branches
be externally visible: while appropriate to model nondeterminism that results
from a lack of information, it does not correspond to true internal
choice. Put another way, thinking of the trees as labeled transition systems, are deterministic.  With , we therefore additionally consider
truly branching nodes, explicitly build the associated nondeterministic ,
and define proper bisimulations on the structure.

The resulting definitions are very expressive. As foreseen, they form a proper monad,
validating all monadic laws up-to coinductive structure equality, they allow us to
establish desired equations such as $p_3 \equiv \cbr{p_2}{p_3}$, but
they also scale to model and cooperative multithreading.

Before getting to that, and to better motivate our definitions, let us further extend
our toy language with a construction that cannot
reduce, and a instruction that simply prints a dot. We will refer to
this language as .

xe c1c2 bc
Consider the program $p \defeq \cbr{(\cwhile{\true}{\cprint})}{\cstuck}$.
Depending on the intended operational semantics associated with , this program can
have one of two behaviors: (1) either to always reactively print an infinite chain
of dots, or (2) to become nondeterministically either similarly reactive, or completely

When working with (small-step) operational semantics, the distinction between
these behaviors is immediately apparent in the reduction rule for (we only show rules for the left branch here).

*[right=BrInternal] c1c2 →c1
*[right=BrDelayed]c_1 →c_1'c_1c_2 →c_1'

BrInternal specifies that may simply reduce to the left branch,
while BrDelayed specifies that can reduce to any state
reachable from the left branch.
From an observational perspective, the former situation describes a system where,
although we do not observe which branch has been taken, we do observe that
a branch has been taken. On the contrary, the latter only progresses if one of the branches can progress, we thus directly observe the subsequent evolution of the chosen branch, but not the branching itself.

In order to design the right monadic structure allowing for enough flexibility
to model either behavior, it is useful to look ahead and anticipate how we will
reason about program equivalence, as described in detail in
Section <ref>.
The intuition we follow is to  interpret our computations as labeled transition systems and
define bisimulations over those, as is generally done in the process algebra literature.
From this perspective, the program $p$ may correspond to three distinct LTSs
depending on the intended semantics, as shown in Figure <ref>.

node distance=2cm,
every state/.style=

minimum size=30pt,
thick, fill=gray!10
every loop/.style=
looseness=4, in=70,out=110,
initial text=$ $,

[state] (1) $p$;
[state, right of=1] (2) $reac$;
[state, above of=1] (3) $stuck$;

(1) edge[align=center] node[sloped]
(1) edge[align=center] node[sloped]
(2) edge[loop above,align=center] node

Observation: branches

[state] (1) $p$;
[state, right of=1] (2) $reac$;
[state, above of=1] (3) $stuck$;

(1) edge[below] node[sloped]$\tau$  (2);
(1) edge[above] node[sloped]$\tau$ (3);
(2) edge[loop above, align=center] node

Observation: branching

[state] (1) $p$;
[state, right of=1] (2) $reac$;

(1) edge[align=center] node
(2) edge[loop above,align=center] node

Observation: none

Three possible semantics for the program $p$, from an LTS perspective

Figure <ref> describes the case where picking a branch is an unknown external event, hence where taking a specific branch is an observable action with a dedicated label:
this situation is naturally modeled by a node in the style of
, that is
$\sembra{\cbr{p}{q}} \defeq \Vis{\ebr}{\lambda b \cdot \text{if } b \text{ then }
\sembra{p} \text{ else } \sembra{q}}.$

Figure <ref> corresponds to BrInternal: both the stuck and
the reactive states are reachable, but we do not
observe the label of the  transition. This transition exactly corresponds to the internal
$\tau$ step of process algebra.
This situation is captured by introducing a new kind of node in our data structure,
a branch,
that maps in our bisimulations defined in Section <ref> to
a nondeterministic internal step.
For this semantics, we thus have $\sembra{\cbr{p}{q}} \defeq \brS{2}{\lambda b \cdot \text{if } b \text{ then }
\sembra{p} \text{ else } \sembra{q}}.$[The 2 indicates the arity of
the branching.]

Figure <ref> corresponds to
BrDelayed but raises the question: how do we build such a behavior?
A natural answer can be to
assume that it is the responsibility of the model, i.e., the function mapping
's syntax to the semantic domain, , to explicitly build this LTS.
Here, $\sembra{p}$ would be an infinite sequence of nodes, containing no other node.  While that would be
convenient for developing the meta-theory of , this design choice would
render them far less compositional (and hence less useful) than we want them to
be. Indeed, we want our models to be defined as computable functions by
recursion on the syntax, whenever possible. But to build this LTS directly, the
model for pq needs to introspect the models for p and
q to decide whether they can take a step, and hence whether it
should introduce a branching node. But, in general, statically determining
whether the next reachable instruction is is intractable, so that
introspection will be hard (or impossible) to implement. We thus extend with a third category of  node, a node, which does not directly
correspond to states of an LTS.  Instead, nodes aggregate sub-trees
such that the (inductively reachable) children of a node are “merged”
in the LTS view of the .

This design choice means that, for the BrDelayed semantics, the model
is again trivial to define: $\sembra{\cbr{p}{q}} \defeq \brD{2}{\lambda b \cdot \text{if } b \text{ then }
\sembra{p} \text{ else } \sembra{q}}$, but the definition of
bisimilarity for ensures that the behavior of $\sembra{p}$ is exactly
the LTS in Figure <ref>.

Although BrDelayed and its corresponding LTS in
Figure <ref> is one example in which nodes are
needed, we will see another concrete use in modeling in
Section <ref>.  Similar situations arise frequently, for modeling
mutexes, locks, and other synchronization mechanisms (e.g., the “await”
construct in Encore <cit.>), dealing with crash failures in
distributed systems, encoding relaxed-consistency shared memory models (e.g.,
the ThreadPromise rule of promising
semantics <cit.>).  The construct is needed whenever the
operational semantics includes a rule whose possible transitions depend on the
existence of other transitions, i.e. for any rule of the shape shown below, when
it may sometimes be the case (usually due to nondeterminism) that
$P \not \rightarrow$:

\[
\inferrule*[right=ContingentStep]{P \rightarrow P'}{C[P] \rightarrow C[P']}
\]

The point is that to implement the LTS corresponding to ContingentStep
without using a node would require introspection of $P$ to determine
whether it may step, which is potentially non-computable.  The node
bypasses the need for that introspection at representation time,
instead pushing it to the characterization of the as an LTS, which is
used only for reasoning about the semantics.  The presence of the nodes retains the constructive aspects of the model, in particular the ability
to interpret these nodes at later stages, for instance to obtain an
executable version of the semantics.

§ CTREES: DEFINITION AND COMBINATORS

§.§ Core definitions

(* Core datatype *)
CoInductive ctree (E : Type -> Type) (R : Type) :=
| Ret (r : R)                                         (* a pure computation *)
| Vis X : Type (e : E X) (k : X -> ctree)           (* an external event *)
| brS (n : nat)  (k : fin n -> ctree)                 (* stepping branching *)
| brD (n : nat)  (k : fin n -> ctree)                 (* delayed branching *)

(* Bind, sequencing computations *)
CoFixpoint bind E T U (t : ctree E T) (k : T -> ctree E U) : ctree E U :=
match u with
| Ret r    => k r
| Vis e h => Vis e (fun x => bind (h x) k)
| brS n h => brS n (fun x => bind (h x) k)
| brD n h => brD n (fun x => bind (h x) k)

(* Unary guards *)
Definition Guard (t : ctree E R) : ctree E R := brD 1 (fun _ => t)
Definition Step    (t : ctree E R) : ctree E R := brS 1 (fun _ => t)

(* Main fixpoint combinator *)
CoFixpoint iter I: Type (body : I -> ctree E (I + R)) : I -> ctree E R :=
bind (body i) (fun lr => match lr with
| inr r => Ret r
| inl i => Guard (iter body i)

Notation "E  > F" := (forall X, E X -> F X)
(* Atomic ctrees triggering a single event *)
Definition trigger : E  > ctree E := fun R (e : E R) => Vis e (fun x => Ret x)
(* Atomic branching ctrees *)
Definition brS : ctree E (fin n) := fun n => brS n (fun x => Ret x)
Definition brD : ctree E (fin n) := fun n => brD n (fun x => Ret x)

: definition and core combinators (Core/CTreeDefinitions.v42)

We are now ready to define our core datatype, displayed in the upper part of
Figure <ref>.
The definition remains close to a coinductive implementation of the free monad, but hardcodes
support for an additional effect: unobservable, nondeterministic branching.
The datatype, much like an , is parameterized by a signature of
(external) events E encoded as a family of types, and a return type R.
It is defined as a coinductive tree[The actual implementation uses
a negative style with primitive projections. We omit this technical detail in
the presentation.]
with four kind of nodes: pure computations (Ret),
external events (Vis),
internal branching with implicitly associated $\tau$ step (brS),
and delayed internal branching (brD).
The continuation following external events is indexed by the return type
specified by the emitted event.
For the sake of simpler exposition, we restrict both internal
branches to be of finite width: their continuation are
indexed by finite types fin, but this is not a fundamental
limitation.[We actually also support another branch
that defines enhanced , with arbitrary branching
over indexes specified in the type of the data structure by an
interface akin to E. It is not linked here for anonymity reasons, but
should the paper be accepted, we will add it to the artifact. It is only
used for the material described in this paper for Lemma <ref>.]
When  using finite branching, we abuse notation and write, for instance,
$\brS{2}{t~u}$ for the computation branching with two branches, rather
than explicitly spelling out the continuation which  branches on the choice
index: $\ilc{fun i => match i with 0 => t | 1 => u end}$.

The remainder of Figure <ref> displays (superficially simplified)
definitions of the core combinators.
As expected, ctree E forms a monad for any interface E: the
bind combinator simply lazily crawls the potentially infinite first tree,
and passes the value stored in any reachable leaf to the continuation.
The iter combinator is central to encoding looping and recursive features:
it takes as argument a body, body, intended to be iterated, and is defined
such that the computation returns either a new index over which to continue iterating, or
a final value; iter ties the recursive knot.
Its definition is analogous to the one for , except that we need to ask
ourselves how to guard the cofix: if body is a constant, pure
computation, unguarded corecursion would be ill-defined. use a node for this purpose.
Here, we instead use a unary delayed branch
as a guard, written . We additionally
write for the unary stepping branch—we will discuss how they relate in Section <ref>.
The minimal computations respectively triggering an event e, generating observable
branching, or delaying a branch, are defined as trigger, $Br_S^n$, and $Br_D^n$.

Convenience in building models comes at a cost: many represent the same LTS.
Figure <ref> illustrates this  by defining
several implementing the stuck LTS and the silently spinning one.
The stuckS and stuckD correspond to internal choices with no outcome, while stuckE
is a question to the environment that cannot be answered, leaving the computation hanging;
the spinD* trees are infinitely deep, but never find in their structure a transition to take.
We define formally the necessary equivalences on computations to prove this
informal statement in Section <ref>.

The astute reader may wonder whether both kind of branching nodes
really are necessary. While convenient, we show
in Section <ref> that $\brSn$
can  be expressed in terms of $\brDn$ and $\step$.

node distance=2cm,
every state/.style=

minimum size=30pt,
thick, fill=gray!10
every loop/.style=
looseness=4, in=70,out=110,
initial text=$ $,

(* Stuck processes *)
Definition stuckE (e : E void) : ctree E void := trigger e
Definition stuckS : ctree E void := brS 0
Definition stuckD : ctree E void := brD 0
CoFixpoint spinD  : ctree E R := Guard spinD
CoFixpoint spinD_nary n : ctree E R := brD n ;; spinD_nary n

[state] (1) $stuck$;

(* Spinning processes *)
CoFixpoint spinS : ctree E R := Step spinS
CoFixpoint spinS_nary n : ctree E R := brS n ;; spinS_nary n

[state] (1) $spin$;
(1) edge[loop above,align=center] node[sloped]$\tau$ (1);

Concrete representations of stuck and spinning LTSs

§.§ A hint of introspection: heads of computations

nodes avoid the need for introspection on trees to model something as generic as a delayed
branching construct such as the one specified by BrDelayed.
However, introspection becomes necessary to build a tree that depends on the
reachable external actions of the sub-trees.
This is the case for example for 's parallel operator that we model in Section <ref>.
The set of reachable external actions is not computable in general, as we may have to first know if the
computation to the left of a sequence terminates before knowing if the events
contained in the continuation are reachable.
We are, however, in luck, as we have at hand a semantic domain able to represent
potentially divergent computations: themselves!

Variant action E R :=
| ARet (r : R)
| ABr  n (k : fin n -> ctree E R)
| AVis X (e : E X) (k : X -> ctree E R).

CoFixpoint head E X (t : ctree E X) : ctree E (action E X) :=
match t with
| Ret x => Ret (ARet x) | Vis e k => Ret (AVis e k) | brS n k => Ret (ABr k)
| BrD n k => BrD n (fun i => head (k i))

Lazily computing the set of reachable observable nodes (Misc/Head.v1)

The head combinator, described on Figure <ref>, builds a
pure, potentially diverging computation
only made of delayed choices, and whose leaves contain all reachable
subtrees starting with an observable node.
These “immediately” observable trees are captured in an action datatype, which is used
as the return type of the built computation. The head[The head t computation could be typed at the empty interface. It is in practice simpler to directly type it at the same interface as the t.] combinator simply crawls the
tree by reconstructing all delayed branches, until it reaches a subtree with any other node at its root; it then returns that subtree as the corresponding action.

§ EQUIVALENCES AND EQUATIONAL THEORY FOR

Section <ref> introduced , the domain of computations we consider,
as well as a selection of combinators upon it. We now turn to the question of
comparing computations represented as for notions of equivalence
and refinement. In particular, we formalize the LTS
representation of a that we have followed to justify our definitions.
This section first introduces a (coinductive) syntactic equality of
, then it recovers the traditional notions of strong and weak
bisimilarity of processes, as well as trace equivalence, for an LTS
derived from the tree structure.  We equip these notions with a
primitive equational theory for ; this theory provides
the building blocks necessary for deriving domain-specific equational
theories, such as the ones established in Section <ref> for , and in
Section <ref> for cooperative scheduling.

§.§ Coinductive proofs and up-to principles in Coq

Working with requires the use of several coinductive predicates and
relations to describe equivalences, refinements and invariants.
Doing so at scale in would be highly impractical if only using its native
support for coinductive proofs, but it is nowadays more feasible thanks to
library support <cit.>.

Our development relies on Pous's
library <cit.> to
define and reason about the various coinductive predicates and relations we
manipulate. We briefly recall the essential facilities, based
on the companion <cit.>, that the library provides.
In particular, we define a subset of candidate “up-to” functions—we indicate
in the subsequent subsections which ones constitute valid up-to principles for
respectively the structural equality and the strong bisimulation we manipulate.
Note: this section is aimed at the reader interested in understanding the internals of
our library: it can be safely skipped at first read.

The core construction provided by the library is a operator (b:X)
for any complete lattice X, and monotone endofunction $b : \ilc{X} \to \ilc{X}$.
In particular, the sort of propositions Prop forms a
complete lattice, as do any function
from an arbitrary type into a complete lattice—coinductive relations, of
arbitrary arity, over arbitrary types, can therefore be built using this combinator.
We most often instantiate X with the complete
lattice of binary relations over : X := ctree E A -> ctree E A ->
Prop for fixed parameters E and A.
We write such binary relations as rel(A,B) for
A -> B -> Prop, and rel(A) for rel(A,A);
for instance: X := rel(ctree E A).

The library provides tactic support for   coinductive proofs based on
Knaster-Tarski's theorem: any is below the .
Specialized to relations on , the proof
method consists in exhibiting a relation R, that can be thought of as a
set of pairs of trees, providing a “coinduction candidate”, and
proving that (forall t u, R t u -> b R t u) -> forall t u, R t u -> gfp b t

The major benefit of the companion is, however, to further provide support for
proofs by enhanced coinduction.

Given an endofunction $b$, a (sound) enhanced coinduction principle,
also known as an up-to principle, relies on an additional function
$f$: X -> X allowing one to work with bf (the composition of $b$ with $f$) instead of $b$:
any of $bf$ is below the of $b$. Concretely, the user has now access to a new proof principle.
Rather than having to “fall back” exactly into their coinduction hypothesis after “stepping”
through $b$, they may first apply $f$. In the case of a coinductive relation,
simple examples of up-to principles include adding the diagonal or swapping the arguments,
allowing one to conclude by reflexivity or invoke symmetry regardless of the coinduction candidate considered.

Significant effort has been invested in identifying classes of sound up-to
principles, and developing ways to combine them <cit.>.
The companion relies on one particular sub-class of sound principles that forms a complete lattice,
the compatible functions: we hence can conduct
proofs systematically up-to the greatest compatible function, dubbed the
companion and written b.

In practice, this means that
a coinductive proof can, on-the-fly, use any
valid up-to principle drawn from the companion.
We refer the interested reader to the literature <cit.> and
our formal development for further details, and
describe below the  specialization to of the up-to functions we use.

R {(x,x)} R {(y,x) | R x y} R {(x,z) | ∃y, R x yR y z} R {(ek,ek') | ∀v, R (k v) (k' v)}equiv  R {(xk,yl) | equiv x y ∀v,R (k v) (l v)}equiv  R {(x,y) | ∃x' y', equiv x x'R x' y' equiv y' y}

Main generic up-to principles used for relations of where
R : rel (ctree E X)

Figure <ref> describes the main generic up-to principles we use for our
relations on .[These are the core examples of library level up-to principles we provide. For our case study, we also prove the traditional language level ones.]
Note that since we are considering relations on , each of these principles, these candidates “$f$”, are endofunctions of relations: for instance, is the constant diagonal relation, builds the symmetric relation, is the composition of relations.
The validity of , and for a given endofunction $b$ entails respectively the reflexivity, symmetry and
transitivity of the relations $(b\compa{b}\;R)$ and $(\compa{b}\;R)$.
These two relations are precisely the ones involved during a proof by
coinduction up-to companion: the former as our goal, the latter as our
coinduction hypothesis.

The and _ up-to functions help when reasoning structurally, respectively
allowing to cross through nodes and  constructs during proofs by coinduction.
Finally, validity of the equiv principle allows for rewriting
via the $equiv$ relation during coinductive proofs for $b$.

§.§ Coinductive equality for

Coq's equality, eq, is not a good fit to express the structural equality
of coinductive structures—even the eta-law for a coinductive data structure does
not hold up-to eq. We therefore define, as is standard, a structural
equality[Note that for , this relation corresponds to what
dub as strong bisimulation, and name eq_itree. We carefully avoid
this nomenclature here to reserve this term for the relation we define in Section <ref>]
by coinduction equ: rel(ctree E A) (written  in infix).
The endofunction simply matches head constructors and behaves extensionally on continuations.

Structural equality (Eq/Equ.v32)

\begin{align*}
\equn \defeq \gfp{R}
& \{(\Ret{v},~\Ret{v})\}~\cup
\{(\Vis{e}{k},~\Vis{e}{k'})~\mid~\forall v,~\gfpc{R}~(k~v)~(k'~v)\} ~\cup\\
&\{(\brD{n}{k},~\brD{n}{k'})~\mid~\forall v,~\gfpc{R}~(k~v)~(k'~v)\} \cup
\{(\brS{n}{k},~\brS{n}{k'})~\mid~\forall v,~\gfpc{R}~(k~v)~(k'~v)\}
\end{align*}

The relation raises no surprises: it is an equivalence relation, and is
adequate to
prove all eta-laws—for the structure itself and for the we manipulate. Similarly, the usual monadic laws are established with respect to .

Monadic laws (Eq/Equ.v838)

v k k v x tx t (t k) l t (λx ⇒k  x l)

Of course, formal equational reasoning with respect to an equivalence relation
other than eq comes at the usual cost: all constructions introduced over
must be proved to respect (in parlance, they must be
Proper), allowing us to work  painlessly with setoid-based

Finally, we establish some enhanced coinduction principles for .
Enhanced coinduction for (Eq/Equ.v167)

$\reflC$, $\symC$, $\transC$, $\bindC{\equ}$ and
$\uptorelC{\equ}$ provide valid up-to principles for $\equn$.

While $\equn$, being a structural equivalence, is very comfortable to work with,
it, naturally, is much too stringent.  To reason semantically about , we need
a relation that remains termination sensitive but allows for differences in
internal steps, that still imposes a tight correspondence over external events,
but relaxes its requirement for nondeterministically branching nodes.  We achieve this by drawing
from standard approaches developed for process calculi.

§.§ Looking at under the lens of labeled transition systems

To build a notion of bisimilarity between computations, we
associate a labeled transition system to a , as defined in
Figure <ref>.
This LTS exhibits three kinds of labels: a [We warn again the reader accustomed to to think of under the lens of the process algebra literature, and not as a representation of 's Tau constructor.]
witnesses a stepping branch,
an ex observes the encountered event together with the answer from the
environment considered, and a v is emitted when returning a value.
Interestingly, there is a significant mismatch between the structure of the
tree and the induced LTS: the states of the LTS correspond to the nodes of the that are not
immediately preceded by a delayed choice.
Accordingly, the definition of the transition relation between states inductively iterates over delayed branches.
Stepping branches and visible nodes map immediately to a set of transitions, one for each outgoing edge; finally

a return node generates a single  transition, moving onto a stuck state,
encoded as a nullary branching node and written .

These rules formalize the intuition we gave in Section <ref> that allowed us to derive the LTSs of Figure <ref>  from the corresponding terms.

ev v

k vltnklt nkk v ekevk v vv

Inductive characterisation of the LTS induced by a (Eq/Trans.v69)

Defining the property of a tree to be stuck, that is: $\isstuck{t} \ \defeq \ \forall l~u,~\lnot (\lstep{t}{l}{u})$, we can make
the depictions from Figure <ref> precise: nullary
nodes are stuck by construction, since stepping would require a
branch, while is proven to be stuck by induction, since it cannot reach any

The stepping relation interacts slightly awkwardly with : indeed,
although a unit for , the Ret construct is not inert from the
perspective of the LTS. Non  transitions can therefore be propagated
below the left-hand-side of a , while a  transition in the prefix
does not entail the existence of a transition in the
—Figure <ref> describes the corresponding lemmas.

tlu   l ≠ vt klu k
tv   k vlut klu
t klu
(l ≠ v ∃t',tlt' u t' k) (∃v,
tvk vlu)

Transitions under bind (Eq/Trans.v953)

We additionally define the traditional weak transition $\wstep{s}{l}{t}$ on
the LTS that can perform tau transitions before or after the $l$ transition
(and possibly be none if $l=\tau$).
This part of the theory is so standard that we can directly reuse parts of the
development for that Pous developed to illustrate the
companion <cit.>,
with the exception that we need to work in a Kleene Algebra with a model closed
under rather than eq.

§.§ Bisimilarity

Having settled on the data structure and its induced LTS, we are back on a
well-traveled road: strong bisimilarity (referred simply as
bisimilarity in the following) is defined in a completely standard way
over the LTS view of .

The progress function $sb$ for  bisimilarity maps a relation
$\mathcal{R}$ over  to the relation such that $sb~R~s~t$ holds if and only if:

\[
\forall l~s',~ \lstep{s}{l}{s'}
\implies
\exists t'.~ s' ~\mathcal{R}~ t'
\land \lstep{t}{l}{t'}
\]

and conversely

\[
\forall l~t',~ \lstep{t}{l}{t'}
\implies
\exists s'.~ s' ~\mathcal{R}~ t'
\land \lstep{s}{l}{s'}
\]

i.e.     [c].35

(s) at (-1,1) $s$;
(R) at (0,1) $sb~\mathcal{R}$;
(t) at (1,1) $t$;
(sp) at (-1,0) $s^\prime$
edge [<-] node[auto] $l$ (s);
(Rp) at (0,0) $\mathcal{R}$;
(tp) at (1,0) $t^\prime$
edge [<-] node[auto,swap] $l$ (t);

Bisimilarity, written $s \sbisim t$, is defined as the
of $sb$: $\sbisimn \defeq \gfptop{sb}.$

All the traditional tools
surrounding bisimilarity can be transferred to our setup.
We omit the details for spacing concerns, but additionally provide:

* weak bisimilarity, written $s \wbisim t$, derived from the
definition of the weak transition (Eq/WBisim.v88);

* a characterization of the traces (represented as colists) of a ,
used to define trace-equivalence (written $\treq$) (Eq/Trace.v15);

* strong simulations (written $\ssim$), defined as the of the half
game for strong bisimulation (Eq/SSim.v31).

§.§.§ Core equational theory

fraction ====
x = y x y

fraction ====
∀x, h xk x eh ek

fraction ====
(∀x,∃y, h xk y) (∀y,∃x, h xk y)nhmk

(∀x,∃y, h xk y) (∀y,∃x, h xk y)nhmk
t u (∀x, g xk x)tg u k

utu t
t(uv) (tu)v
tu ut
tt t
(tu)v tuv
tu ut
tt  t
n  m
(n>0 m>0)(n = m = 0) n  m

Elementary equational theory for (Eq/SBisim.v1008)

Bisimilarity forms an equivalence relation satisfying a collection of
primitive laws for summed up in Figure <ref>.
We use simple inference rules to represent an implication from the
premises to the conclusion, and double-lined rules to represent equivalences.
Each rule is proved as a lemma with respect to the definitions above.

The first four rules recover some structural reasoning on the syntax of the
trees from its semantic interpretation. These rules are much closer to what
provides by construction for :
leaves are bisimilar if they are equal, and computations performing the same
external interaction must remain point-wise bisimilar.
Stepping branches, potentially of distinct arity, can be matched one against
another if and only if both domains of indexes can be injected into the other to
reestablish bisimilarity. In contrast, this condition is sufficient but not
necessary for delayed branches, since the points of the continuation
structurally immediately accessible do not correspond to accessible states in
the LTS. Finally, bisimilarity is a congruence for .

Another illustration of this absence of equivalence for delayed branching nodes
as head constructor is that such a computation may be strongly bisimilar to a
computation with a different head constructor.
The simplest example is that  can ignore (finite numbers of) nodes.

Another example is that stuck processes behave as a unit for delayed branching nodes.
We furthermore obtain the equational theory that we  expect for
nondeterministic effects. Delayed branching is associative, commutative, idempotent,
and can be merged into delayed branching nodes of larger
arity w.r.t. .[Stating these facts generically in the arity of branching is quite
awkward, we hence state them here for binary branching, but adapting them at
other arities is completely straightforward.]
In contrast, stepping branches are only commutative, and almost idempotent,
provided we introduce an additional .
This can  in turn be ignored by moving to weak bisimilarity, making stepping branches commutative and properly idempotent; however, it crucially remains not associative, a standard fact in process algebra.[This choice would be referred as external in this community]

Finally, two  delayed spins are always
bisimilar (neither process can step) while two stepping spins
are bisimilar if and only if they are  both
nullary (neither one can step), or both non-nullary.

We omit the formal equations for sake of space here, but we additionally prove
that the iter combinator deserves its name: the Kleisli category of the
ctree E monad is iterative w.r.t. strong bisimulation (Eq/IterFacts.v1).
Concretely, we prove that the four equations described in <cit.>,
Section 4, hold true.
The fact that they hold w.r.t. strong bisimulation is a direct consequence of the design choice taken in our definition of iter: recursion is guarded by a .
We conjecture that one could provide an alternate iterator guarding recursion by
a , and recover the iterative laws w.r.t. weak bisimulation, but have not
proved it and leave it as future work.

Naturally, this equational theory gets trivially lifted at the language level for (ImpBr.v125).
The acute reader may notice that in exchange for being able to work with strong
bisimulation, we have mapped the silently looping program to
spinD, hence identifying it with stuck processes.
For an
alternate model observing recursion, one would need to investigate the use of
the alternate iterator mentioned above and work with weak bisimilarity.

§.§.§ Proof system for bisimulation proofs

As is usual, the laws in Figure <ref>, enriched with
domain-specific equations, allow for deriving further equations purely
equationally.  But to ease the proof of these primitive laws, as well
as new nontrivial equations requiring explicit bisimulation proofs, we
provide proof rules that are valid during bisimulation proofs.

∀v, R (k v) (k' v)ekek'
(∀x,∃y, R (k x) (k' y)) (∀y,∃x, R (k x) (k' y))nkmk'
∀v, R (k v) (k' v)nknk'
(∀x,∃y, (k x)(k' y)) (∀y,∃x, (k x)(k' y))nkmk'
tu t u
t R u t u

Proof rules for coinductive proofs of (Eq/SBisim.v673)

Given a bisimulation candidate $R$,
we write $t \sbisimR u$ for $sb~(\compa{sb}~R):$ one needs to “play the
bisimulation game” by crossing $sb,$ and may rely on $R$ to conclude by
coinduction, while furthermore being able to exploit the companion $\compa{sb}$
to leverage sound up-to principles.

We depict the main rules we use in Figure <ref>. These proof
rules are notably convenient because they avoid an
exponential explosion in the number of cases in our proofs, which otherwise
would arise due to the systematic binary split entailed by the natural way to
play the bisimulation game.

These rules essentially match up counterpart constructors at the level of bisimilarity,
but additionally make a distinction as to whether applying the rule soundly acts
as playing the game—i.e., the premises refer to $R$, allowing to
conclude using the coinduction hypothesis—or whether they do not—, i.e., the
premises still refer to $\sbisimR$.
The latter situation arises when using the proof rules that strip off
delayed branches from the structure of our trees: on either side, they do not
entail any step in the corresponding LTSs, but rather correspond to recursive calls to its
inductive constructor.

Furthermore, we provide a rich set of valid up-to principles:
Enhanced coinduction for (Eq/SBisim.v219)

The functions $\reflC$, $\symC$, $\transC$, $\visC$, $\bindC{\sbisim}$,
$\uptorelC{\equ}$ and $\uptorelC{\sbisim}$ provide valid up-to principles for $\sbisimn$.

In particular, the equation $\guard~t\sbisim t$ can be used for rewriting during
bisimulation proofs, allowing for asymmetric stripping of guards.

§.§ Eliminating nondeterministic stepping choices

Out of programming convenience, offer both stepping and delayed
branching of arbitrary arity.
However, as hinted at in Section <ref>, this is
superfluous: a stepping branch can always be simulated by delaying the same
choice, and guarding each branch by a unary . We make this intuition formal
by proving that the following combinator, precisely performing this
transformation, preserves the behavior of the computation with respect to .

Definition BrSElim E X (t : ctree E X) : ctree E X :=
iter (fun t => match t with
| Ret  r   => Ret (inr r)
| brD  k   => x <- brd;; Ret (inl (k x))
| brS  k   => x <- brd;; Step (Ret (inl (k x)))
| Vis  e k => x <- trigger e;; Ret (inl (k x))
end) t.

Stepping nondeterministic branches can be eliminated (Misc/brSElim.v249)
\(\forall t,~\ilc{BrSElim}~t\sbisim t\)

The proof of this statement is quite illustrative of bisimulation proofs over
We provide its sketch in the appendixin the extended version <cit.> as a means to illustrate the layers of facilities put in place in the formal development
to allow for the translation of paper intuitions, most notably the enhanced
coinduction principles that the companion allows us to build. It also
illustrates the difficulties that the structure raises when bridging the distance between the syntax (the tree) and its implicit semantics (the LTS).

§ INTERPRETATION FROM AND TO

The ecosystem fundamentally relies on the incremental interpretation of
effects, represented as external events, into their monadic implementations.
Through this section, we show how fit into this narrative both by
supporting the interpretation of their own external events, and by being
a suitable target monad for , for the implementation of nondeterministic

§.§ Interpretation

support interpretation: provided a handler h:E  > M
implementing its signature of events E into a suitable monad M,
the (interp h):itree E  > M combinator provides an implementation of
any computation into M.
The only restriction imposed on the target monad M is that it must support
its own iter combinator, i.e., be iterative, so that the full
coinductive nature of the tree can be internalized in M.
For this implementation to be sensible and amenable to verification in
practice, one must, however, check an additional property: interp h
should form a monad morphism—in particular, it should map to equivalent monadic computations in M.

Definition interp (h : E  > M) : ctree E  > M := fun R =>
iter (fun t => match t with
| Ret r   => ret (inr r)
| BrD n k => bind (mBrD n) (fun x => ret (inl (k x)))
| BrS n k => bind (mBrS n) (fun x => ret (inl (k x)))
| Vis e k => bind (h e)       (fun x => ret (inl (k x)))

Interpreter for (class constraints omitted) (Interp/Interp.v32)

Unsurprisingly, given their structure, enjoy their own interp
combinator. Its definition, provided in Figure <ref>, is very close
to its counterpart.  The interpreter relies on the version of
iter, chaining the implementations of the external events in the process.
The target monad must naturally still be iterative, but must also explain how it
internalizes branching nodes through the mBrD and mBrS operations.

Perhaps more surprisingly, the requirement that interp h define a monad
morphism unearths interesting subtleties.
Let us consider the elementary case where the interface E is implemented in terms
of (possibly pure) uninterpreted computations, that is when M := ctree F.
The requirement becomes: $\forall t~ u, t \sbisim u \rightarrow \ilc{interp h}~t
\sbisim \ilc{interp h}~u.$
But this result does not hold for an arbitrary h: intuitively, our
definition for has implicitly assumed that implementations of external
events may eliminate reachable states in the computation's induced LTS—through pure implementations—but should not be allowed to introduce new ones.

[[$0$] [$1$]]
[[$2$] [$3$]]]

[[$2$] [$1$]]
[[$0$] [$3$]]]

[[[$0$] [$1$]]]
[[[$2$] [$3$]]]]

[[[$2$] [$1$]]]
[[[$0$] [$3$]]]]

Two strongly bisimilar trees before interpretation (left), but not after (right)

The counter-example in Figure <ref>,
where $\ebr$ is the binary event introduced in Section <ref>,
fleshes out this intuition. Indeed, both trees are strongly bisimilar:
each of them can emit the label $\lobs{\ebr}{\false}$ by stepping to either the
$\Ret{0}$ or $\Ret{2}$ node, or emit the label
$\lobs{\ebr}{\true}$ by stepping to either the
$\Ret{1}$ or $\Ret{3}$ node.
However, they are  strongly bisimilar because the induced LTS  processes the question to the environment—$\ebr$— and its
answer—$\false/\true$—in a single step, such that the computations never
observe that they have had access to distinct continuations.

However, if one were to introduce in the tree a node before the external
events, for instance using the handler h := fun e => Step (trigger e),
a new state allowing for witnessing the distinct continuations would become
available in the LTSs, leading to non-bisimilar interpreted trees.

We hence say a handler h : E  > ctree F is simple if it implements
each event e either as a pure leaf, i.e., h e = Ret x, or simply
translates it, i.e., h e = trigger f.
Similarly, we say that h : E  > stateT S (ctree F) is simple if it is
point-wise simple.
We show that we recover the desired property for the subclass of simple handlers:

* If h : E  > ctree F is simple, then $\forall t~u,~t\sbisim u \rightarrow$ interp h $ t \sbisim $ interp h $ u.$

* If h : E  > stateT (ctree F) is simple, then $\forall
t~u,~t\sbisim u \rightarrow \forall s,$ interp h $ t~s \sbisim $
interp h $ u~s.$

The latter result is, in particular, sufficient to transport equations
established before interpretation—such as the theory of $\_$$\_$—through
interpretation (ImpBr.v174). More generally, we can reason after
interpretation to establish equations relying both on the nondeterminism and
state algebras, for instance to establish the equivalence $p_3
\equiv \cbr{p_2}{p_3}$ mentioned in Section <ref> (ImpBr.v213).

§.§ Refinement

Interpretation provides a general theory for the implementation of external events.
Importantly, also support an analogous facility for the refinement of its
internal branches: one can shrink the set of accessible paths in a computation—and, in particular, determinize it.

Definition refine (h : bool -> forall (n:nat), M (fin n)) : ctree E  > M := fun R =>
iter (fun t => match t with
| Ret r   => ret (inr r)
| BrD n k => bind (h false n) (fun x => ret (inl (k x)))
| BrS n k => bind (h true  n) (fun x => ret (inl (k x)))
| Vis e k => bind (mtrigger e) (fun x => ret (inl (k x)))

Refiner for (class constraints omitted) (Interp/Refine.v17)

We provide, to this end, a new combinator, refine, defined in Figure <ref>.
Similar to interp, it takes as an argument a handler specifying how to
implement our object of interest into a monad M. Since here we are
interested in the implementation of branching nodes, the handler describes how
to monadically choose a branch—the boolean flag allows for different
behaviors between delayed and stepping branches.[This definition
becomes even more uniform with interp once we allow for parameterized,
arbitrary indexing of branching nodes, as  in the enhanced branch of our  development.]
As usual, the implementation monad must be iterative, but this time it must also
specify how to re-embed the external events using an operation called mtrigger (a concept already used in  <cit.>).

Definition refine_cst (h : bool -> forall (n:nat), fin (S n)) : ctree E  > ctree E :=
refine (fun b n => match n with
| O => stuckD
| S n => if b then Step (Ret (h b n)) else Guard (Ret (h b n))

Definition refine_state (h : St -> forall (b:bool) (n:nat), St * fin (S n))
: ctree E  > stateT St (ctree E) :=
refine (fun b n s => match n with O => stuckD | S n => Ret (h s b n)  end).

Constant and stateful refinements (Interp/Refine.v51)

As hinted at by the combinator's name,
the source program should be able to simulate the refined program.
Fixing M to ctree F, this is expressed as
$\forall t,~$refine h$~t \ssim t$.
However, one cannot hope to obtain such a result for an arbitrary h, because it
could implement internal branches with an observable computation that can't be
simulated by $t$.

We hence provide two illustrative families of well-behaved refinements, depicted on
Figure <ref>.
Constant refinements, implemented into ctree E, lift a function systematically,
returning the same branch given the nature and arity of the branching node.
Stateful refinements carry a memory into a piece of state St and implement
the refinement into stateT St (ctree E) by using the current state to pick
a branch, and update the state. A particular example of such a stateful
refinement is a round-robin scheduler.

The constant and stateful refinements are proper refinements
[The second theorem actually cannot
be stated in the main development provided as artifact: the return types of the
trees are not identical — the refined tree computes additionally a final
state. We prove it in the enhanced branch with
support for heterogeneous relations and arbitrary relations on labels.]

\begin{align*}
\forall h~t,~\ilc{refine_cst}~h~t\ssim t \qquad \mathrm{and} \qquad
\forall h~t~s,~\ilc{refine_state}~h~t~s\ssim t    % \end{mathpar}
\end{align*}

Finally, the shallow nature of also offers testing opportunities.
<cit.> describe how external events such as IO interactions
can alternatively be implemented in and linked against at extraction.
Similarly, we demonstrate on how to execute a by running an impure refinement
implemented in by picking random branches along the execution.

§.§ ITree embedding

We have used directly as a domain to represent the syntax
of , as well as in our case studies (see Section <ref> and <ref>).
can, however, fulfill their promise sketched in
Section <ref>, and be used as a domain to host the monadic implementation of
external representations of nondeterministic events in an .

Definition inject E : itree E  > ctree E := interp (fun e => trigger e).
Definition internalize E : ctree (Choose +' E)  > ctree E :=
interp (fun e => match e with | inl1 (choose n) => brs | inr1 e => trigger e).
Definition embed E : itree (Choose +' E)  > ctree E :=
fun _ t => internalize (inject t).

Implementing external branching events into the monad (Interp/ITree.v24)

To demonstrate this approach, we consider the family of events choose (n: nat) : Choose (fin n),
and aim to define an operator embed taking an computation modeling
nondeterministic branching using these events, and implementing them as stepping
branches into a .
This operator, defined in Figure <ref>, is the composition of two
transformations. First, we inject into by () interpretation.
This injection rebuilds the original tree as a , where nodes
have become Guard nodes, and an additional Guard has been introduced
in front of each external event.
Second, we internalize the external branching contained in a implementing a Choose event, using the isomorphic stepping branch.
The resulting embedding forms a monad morphism transporting into :

embed respects (Interp/ITree.v346)

\(
\forall t~u, \euttn~ t~ u \implies embed(t)\sbisim embed(u)
\)

The proof of this theorem highlights how nodes in collapse
two distinct concepts that nondeterminism forces us to unravel in .
The relation is defined as the of an inductive endofunction euttF.
In particular, one can recursively and asymmetrically strip finite amounts of —the corecursion is completely oblivious to these nodes in the structures.
Corecursively, however, nodes can be matched symmetrically—a construction that is useful in exactly one case, namely to relate the silently spinning computation, $\itau^{\omega},$ to itself.
From the perspective, recursing in euttF corresponds to recursion in
the definition of the LTS: nodes are nodes.
But corecursing corresponds to a step in the LTS: $\itau^{\omega}$ corresponds to $\step^{\omega}$.
' thus corresponds to either a or a .
Nondeterminism forces us to separate both concepts, as
whether a node in the tree constitutes an accessible state in the LTS

becomes semantically relevant. We obtain two "dual"
notions that have no equivalent in : we may have finite amounts of
asymmetric corecursive choices, i.e., finitely many s, and
structurally infinite stuck processes, i.e., $\guard^{\omega}$.

In the proof of Lemma <ref>, this materializes by the fact that an induction
on euttF leaves us disappointed in the symmetric case: we have no
applicable induction hypothesis, but expose in our embedding a $\guard$,
which does not allow us to progress in the bisimulation. We must resolve the
situation by proving that being able to step in embed t implies
that t is not $\itau^{\omega}$, i.e., that we can inductively
reach a Vis or a Ret node (Interp/ITree.v276).

Limitations: on guarding recursive calls using .
We have shown that equipped with iter as recursor and strong
bisimulation as equivalence form an iterative monad. Furthermore, building
interpretation atop this iter combinator gives rise to a
monad morphism respecting , hence is suitable
for implementing non-deterministic effects represented as external in an

However, we stress that the underlying design choice in the definition of
iter, guarding recursion using , is not without consequences.
It has strong benefits, mainly that a lot of reasoning can be performed against strong
bisimulation. More specifically, this choice allows the user to reserve weak
bisimulation for the purposes of ignoring domain-specific steps of computations that may be relevant
both seen under a stepping or non-stepping lens—e.g., synchronizations
in —but it does not impose this behavior on recursive calls.
However, it also leads to a coarse-grained treatment of silent divergence:
in particular, the silently diverging (an infinite chain of ) is embedded into an
infinite chain of , which, we have seen, corresponds to a stuck LTS.
For some applications—typically, modeling other means of being
stuck and later interpreting them into a nullary branch—one would
prefer to embed this tree into the infinite chain of to avoid equating
both computations. While one could rely on manually introducing a in the
body iterated upon when building the model, that approach is a bit cumbersome.

Instead, a valuable avenue would be to develop the theory accompanying the
alternate iterator mentioned in Section <ref> and guarding
recursion using .  Naturally, the corresponding monad would not be
iterative with respect to strong bisimulation, but we conjecture that it would
be against weak bisimulation.  From this alternate iterator would arise an
alternative embedding of into : we conjecture it would still
respect , but seen as a morphism into equipped with weak
bisimulation. The development accompanying this paper does not yet support this
alternate iterator, we leave implementing it to future work.

Currently, the user has the choice between (1) not
observing recursion at all, but getting away with strong bisimulation in
exchange, (2) manually inserting at recursive calls that they chose to
observe. With support for this alternate iterator, the user
would be given additional option to (3) systematically -observe recursion,
at the cost of working with weak bisimulation everywhere.

§ CASE STUDY: A MODEL FOR CCS

We claim that form a versatile tool for building semantic models of
nondeterministic systems, concurrent ones in particular. In this section, we
illustrate the use of as a model of concurrent communicating processes
by providing a semantics for Milner's Calculus of
Communicating Systems () <cit.>. The results we obtain—the usual
algebra, up-to principles, and precisely the same equivalence relation as the
usual operational-based strong bisimulation—are standard, per se, but
they are all established by exploiting the generic notion of bisimilarity of . The result is a
shallowly embedded model for in Coq that could be easily, and modularly, combined with other
language features.

§.§ Syntax and operational semantics

l::=  τ ::=  l

a P a P
P l P'P Q l P'
Q l Q'P Q l Q'
P l P'P Q l P' Q
Q l Q'P Q l P Q'
P P'   Q  Q'P Q τP' Q'
P l P'   l {,}P l P'
P ∥P l P'P l P'

Syntax for (Syntax.v51) and its operational semantics (Operational.v12)

The syntax and operational semantics of are shown in Figure <ref>.
The language assumes a set of names, or communication channels, ranged over by $\comm$.
For any name $\comm,$ there is a co-name $\bar \comm$ satisfying
$\bar {\bar \comm} = \comm$. An action is represented
by a label $l$; it is either a communication label $\comm$ or $\bar\comm$,
representing the sending/reception of a message on a channel, or the reserved
action $\tau$, which represents an internal action.

The standard operational semantics, shown in the figure, is
expressed as a labeled transition system, where states are terms $P$ and labels
are actions $l$. The operators are the following: $\pnil$ is the process with
no behavior. A prefix process ${\prf l P}$ emits an action $l$ and then becomes
the process $P$. The internal choice $\pls\pP\pQ$ behaves either like the
process $\pP$ or like the process $\pQ$, in the same fashion as the
BrInternal semantics for in Section <ref>.
The parallel composition of two processes $\para\pP\pQ$ interleaves
the behavior of the two processes, while allowing the two processes to
communicate. If the process $\pP$ emits a name $\comm$ and the process $\pQ$
emits its co-name $\bar\comm$, then the two processes can progress simultaneously
and the parallel composition emits an internal action $\tau$. Channel
restriction $\new\comm\pP$ prevents the process $\pP$ from emitting an action
$\comm$ or $\bar\comm$: the operational rule states that any emission of another
action is allowed. Finally the replicated process $\bang{\pP}$ behaves as an
unbounded replication of the process $\pP$. Operationally, $\bang{\pP}$ has the
behavior of $\para P {\bang{\pP}}$.

§.§ Model

a p ap
p q pq
p p p

cP  h_new  c  P
where h_new c e =

if e= act  c   or  e=  act  c̅

e   otherwise

pq F  p  q ·

(p'p F q p')

(q'q F p q')

(p'pq'qactLR F p' q')

F q   (nk) n(λi ·F  (k i) q)

F q  (ek) e(λi ·F  (k i) q)

F p  (nk) n(λi ·F  p (k i))

F p  (ek) e(λi ·F  p (k i))

F  r r' {

·F  (k ()) (k' ())       if  ∃a.   r=(act  a)k r'=(act a̅)k'

Denotational model for using as a domain (Denotation.v62)

We define a denotational model for using ctree actE void as domain,
written in the following.
As witnessed by this type, processes do not return any value, but may emit actions
modeled as external events expecting unit for answer: Inductive actE
::= | act a : actE unit.
Figure <ref> defines the semantic operators
associated with each construct of the language. They are written as over-lined
versions of their syntactic counterparts, and defined over .

The empty process is modeled as a stuck tree—we cannot observe it.  Actions
are directly defined as visible events, and thus the prefix triggers the action,
and continues with the remaining of the process.  As discussed in
Section <ref>, the delayed branching node fits exactly with
the semantics of the choice operator in , only progressing if one of the
composed terms progresses.  Restriction raises a minor issue: the compositional
definition implies that the for the restricted term has already been
produced when we encounter the restriction and, a priori, that tree might
contain visible actions on the name being restricted. We enforce scoping by
replacing those actions by a stuck tree, $\stuck$, effectively cutting these
branches.  This is done using the  operator from , with
h_new, a handler that does the substitution.

Parallel composition is more intricate, as the operator
requires significant introspection of the composed terms. The traditional
operational semantics of is not explicitly constructive:
each of the three reduction rules depends on the existence of specific
transitions in the sub-processes.

Depiction of the tree resulting from $\spara{p}{q}$

We perform this necessary introspection, in a constructive way, defining the
tree as an explicit cofixpoint, and using the  operator introduced in
Section <ref>.  While the operation p precisely captures
the desired set of actions that $p$ may perform, computing this set could, in
general, silently diverge. We therefore cannot bluntly initiate the computation
by sequencing the heads of $p$ and $q$, as divergence in the former may render
inaccessible valid transitions in the latter.[Technically, the variant
of considered here actually cannot generate such a computation, so we
could therefore rule this case out extensionally. The case could, however,
easily arise in a variant of relying on recursive processes rather than
replication, and in other calculi, so we therefore favor this more general,
reusable, approach.]  Instead, we initiate the computation with a ternary
delayed choice: the left (resp.  middle) branch captures the behaviors starting
with an interaction by $p$ (resp. $q$), while the right branch captures the
behaviors starting with a synchronisation between $p$ and $q$. Essentially, the
tree nondeterministically explores the set of applicable instances of the three
operational rules for parallel composition.  In particular,
if the operational rule to step in the left (resp. right) process is
non-applicable, the left (resp. middle) branch of the resulting tree silently
diverges.  The right branch silently diverges if neither process can step, but,
in general, it also contains branches considering the interaction of
incompatible actions; we cut these branches by inserting .  In all cases,
the operator continues corecursively, having progressed in either or both
processes.  Figure <ref> shows the resulting from $\spara{p}{q}$.

The last operator to consider is the replication $\sbang$. In theory, it
could be expressed in terms of parallel composition directly, as the cofix
$\sbang p \defeq \spara{p}{~\sbang{p}}$. Unfortunately, although it is sound, defining the
$\sbang{}$ operator in this way is too involved for 's syntactic criterion on
to recognize that the corecursive call is guarded under $\spara{}{}$.

To circumvent this difficulty, we use an auxiliary operator,
$\sparabang{p}{q}$,  capturing the parallel composition of a process
$p$ with a replicated process $\bang{q}$.
It nondeterministically explores
the four kinds of interactions that such a process could exhibit: a step in $p$;
the creation of a copy of $q$ performing a step to $p'$, before being composed
in parallel with $p$; the creation of a copy of $q$ synchronizing with $p$; or
the emission of two copies of $q$ synchronizing one with another.  We finally
define the replication operator as $\sbang p \defeq \sparabang{p}{p}$. We omit the formal definition here,
since it is similar to that for $\spara{}{}$, but point out the interested
reader to its formal counterpart (Denotation.v125) or to the appendix.

With these tools at hand, the model $\sembra{\cdot}:~ \ccs \rightarrow \ccssem$
is defined by recursion on the syntax.

Equational Theory

We provide a first validation of our model by proving that it satisfies the expected equational
theory with respect to 's notion of strong bisimulation, enabling the usual
algebraic reasoning advocated for process calculi.

In particular, we prove that our  definition for the replication is
sane in that it validates equationally the expected definition: $\sbang{p}
\sbisim \spara {\sbang{p}}{p}$ (Denotation.v1452).
We also prove an illustrative collection of expected equations satisfied
by our operators (Denotation.v809):

p q q p
p (q r) (p q) r
p p
p p p

p p
p q q p
p (q r) (p q) r

To facilitate these proofs, we first prove sound up-to principles at the level
of for each constructor: strong bisimulation up-to $\sprf{c}{[\cdot]}$,
$\spls{[\cdot]}{[\cdot]}$, $\spara{[\cdot]}{[\cdot]},$ $\sbang{[\cdot]},$
and $\snew{c}{[\cdot]}$ are all valid principles, allowing us to rewrite under
semantic contexts during bisimulation proofs. Additionally to these language-level up-to
principles, we  inherit the ones generically supported by  (Lem. <ref>).

§.§ Equivalence with the operational strong bisimilarity

In addition to proving that we recover in our semantic domain the expected up-to
principles and the right algebra, we furthermore show that the model is sound
and complete with respect to strong bisimulation compared to its
operational counterpart.
We do so by first establishing an asymmetrical bisimulation between and
, matching operational steps over the syntax to semantic steps in the
. We write $\bar l$ for the obvious translation of labels between both LTSs.

A relation $\mathcal{R}:~ rel(\ccs,\ccssem)$ is a strong bisimulation if and only if,
for any label $l$, term $P$, and  tree $q$.

\[
P ~ \mathcal{R} ~ q
\land \stepccs{P}{l}{P'}
\implies
\exists q',~ P' ~\mathcal{R}~ q'
\land \lstep{q}{\bar{l}}{q'}
\]

and conversely

\[
P ~ \mathcal{R} ~ q
\land \lstep{q}{\bar{l}}{q'}
\implies
\exists P'.~ P' ~\mathcal{R}~ q'
\land \lstep{P}{l}{P'}
\]

(s) at (-1,1) $P$;
(R) at (0,1) $\mathcal{R}$;
(t) at (1,1) $q$;
(sp) at (-1,0) $P^\prime$
edge [<-, shorten <=.06cm] node[auto] $l$ (s);
(Rp) at (0,0) $\mathcal{R}$;
(tp) at (1,0) $q^\prime$
edge [<-, shorten <=.04cm] node[auto,swap] $\bar{l}$ (t);
(ccs) at (-0.84,0.27) ccs;

The relation $R \defeq \{(P,q)~\mid~\sembra{P}\sbisim q\}$ is a strong bisimulation.

We derive from this result that the operational and semantic strong
bisimulations define exactly the same relation over :

\( \forall P~Q,~\sembra{P}\sbisim\sembra{Q} \text{ iff } P \sim_{\ccs} Q\)

§ CASE STUDY: MODELING COOPERATIVE MULTITHREADING

As a second case study, we consider cooperative multithreading.
Cooperative scheduling is used in languages such as Javascript, async
Rust, or Akka/Scala actors, but is also a very general model, as preemptive
multi-tasking is equivalent to cooperative scheduling where threads are willing
to yield (i.e., let other threads run) at any time.
We extend the syntax of with two constructs:

xe c1c2 bc c1c2

The command forks two copies of the currently running program, the first
of which first runs $c1$ and the second of which first runs $c2$,
before they each proceed with the rest of the program.
Importantly, $c2$ retains control, and $c1$ will only execute when $c2$ voluntarily yields control or ends.
This yielding of control is achieved by the $\cyield$ statement, which signals
that the current thread stops and lets a new thread run—possibly the same one

This semantics implements a mechanism like the fork system call, which duplicates the current process, but without a possibility for joining threads.
For example, the program

\[
\cseq
\]

forks two copies of the program, with the “main” thread immediately yielding, allowing for either thread to run next.
Its semantics is to first spawn a thread for $\cassign{x}{1}$, then have the
main thread reach the , giving $\cassign{x}{1}$ a chance to run.
Assuming the spawned thread goes next, it runs in sequence $\cassign{x}{1}$ and
after which the main thread recovers control and finishes its execution.
$\cassign{y}{x}$ is part of both threads and is thus executed twice, after each assignment to $x$.

Alternatively, some cooperative scheduling languages <cit.> consider a spawn
operator that simply spawns an independent thread: we can encode this behavior
in several ways.
Notably, if $\tm{spawn}$ always occurs in tail position, there is no
continuation to duplicate. For instance, the program

\[
\cfork{\cassign{x}{1}}
\]

spawns two threads that set $x$ to different values, and terminates.
The two spawned threads can then be scheduled in either order, resulting
in $x = 1$ or $x = 2$ in the final state.
This constraint could be syntactically enforced in the language if relevant.

Alternatively, one can use the command $\cwhile{\true}{\cyield}$ to
“terminate” a thread; for instance to prevent the first thread above from
reaching $\cassign{y}{x}$. With fancier encodings using reserved
shared-variables, nested “joins” and other synchronization operations can be
In this case study, we do not concern ourselves with such extensions, and
restrict ourselves to the formalization of the syntax described above.

§.§ Model

As with the approach described in Section <ref>, the semantics of
the language is defined in two stages.
First, we represent statements as computations of type ctree (YieldE +
SpawnE + MemE) unit, where YieldE and SpawnE
are used to represent and respectively.
The remaining statements of are defined in a standard way—we omit them.
The new event families are defined as follows:

Variant YieldE : Type -> Type :=
| Yield : YieldE unit.

Variant SpawnE : Type -> Type :=
| Spawn : SpawnE bool.

Yield carries no additional information and acts purely as a signal to yield control, and Spawn introduces a binary branch in the , allowing us to store the asynchronous thread in one branch and the main thread that continues running in the other branch.
Formally, these events are used to denote the corresponding statements:

\begin{align*}
\sembra{\cyield} \defeq& \trigger{\ilc{Yield}} \qquad
\sembra{\cfork{c1}{c2}} \defeq& b \gets \trigger{\ilc{Spawn}} \bind \text{if } b \text{ then } \sembra{c1} \text{ else } \sembra{c2}
\end{align*}

The second stage is more complex than the simple stateful
interpretation of standard : we need to interpret the concurrency-related events.
In particular, since the semantics of these events involves scheduling other threads that work
together, we cannot hope to use , as is done with memory events—this
situation is similar to $\spara{}{}$ for , in both cases the combinator
cannot be implemented as a simple fold.
Instead, we define a custom interpreter for Spawn and Yield events,
namely a scheduler operating over a thread pool of threads, each of which is a
that may contain Spawn and Yield events,
and producing a final devoid of these concurrency events.

\[
\begin{array}{rcl}
\schedule~v_0~\NONE &\defeq& \ret \unit \\
\schedule~v_n~\NONE &\defeq& \brS{n}{(\lambda i \cdot \schedule~v_n~\SOME{i})} \qquad \text{for } n > 0\\
\schedule~v_n~\SOME{i} &\defeq \\
\mathrm{if}\ v[i] = \quad& & \mathrm{then} \\
\ret \unit & & \brD{1}{(\lambda \_ \cdot \schedule~v[-i]_{n-1}~\NONE)} \\
\brS{m}{k} & & \brS{m}{(\lambda i' \cdot \schedule~v[i \mapsto k~i']_n~\SOME{i})} \\
\brD{m}{k} & & \brD{m}{(\lambda i' \cdot \schedule~v[i \mapsto k~i']_n~\SOME{i})} \\
\Vis{\ilc{Yield}}{k} & & \brD{1}{(\lambda \_ \cdot \schedule~v[i \mapsto k~\unit]_n~\NONE)} \\
\Vis{\ilc{Spawn}}{k} & & \brS{1}{(\lambda \_ \cdot \schedule~(k~\true :: v[i \mapsto k~\false])_{n+1}~\SOME{i + 1})} \\
\Vis{\ilc{e}}{k} & & \Vis{e}{(\lambda x \cdot \schedule~(v[i \mapsto k~x])_n~\SOME{i})}
\end{array}
\]

The definition of (Par.v626)

As is usual with cooperative scheduling, the thread pool, encoded as a vector, contains a designated
active thread, i.e., the currently running thread.

We write $v_n$ for a vector of size $n$, and vector operations for removing the
$i$-th element as $v[-i]$, updating the $i$-th element to $x$ as $v[i \mapsto
x]$, and adding an element $x$ to the front as $x :: v$
(so $x$ is the new $0$-th element in the resulting vector).

The scheduler, $\schedule$, is defined formally in Figure <ref>.
References to $\schedule$ in its body should be interpreted as corecursive
calls—we abuse notations to lighten the presentation.

It takes two arguments: the thread pool, and the index of the active
thread in the pool. If no thread is active, the second argument is empty, written (we use an option datatype in ).
If there is an active thread, i, the $\schedule$ makes progress in that
Otherwise, $\schedule$ nondeterministically chooses the next thread to run.
If the thread pool is empty, then $\schedule$ emits a returning .
In more detail, there are several ways the active thread may progress.
If the thread performs a branching or a memory operation, the $\schedule$
returns a that also performs the same operation,
and in each branch replaces the active thread (index $i$)
in the thread pool with its continuation.

If the active thread returns, it is removed from the thread pool; there is no active thread after the removal.
If the thread yields, then $\schedule$ removes the Yield and starts
scheduling with no active thread (which will nondeterminstically pick a new active thread, potentially the same one again).
If the thread spawns a new thread, then $\schedule$ adds the $\true$ branch of
that thread to the thread pool, updates the active thread to the $\false$
branch, and continues running on the $\false$ branch (note that this shifts the active thread from index $i$ to $i+1$).

Using $\schedule$, we can interpret the $\ilc{Yield}$ and $\ilc{Spawn}$ events in concert, allowing us to eliminate them from the .
We denote this “scheduled” semantics by  $\ssembra{p} \defeq
\schedule~[\sembra{p}]_1~\NONE: \ilc{ctree MemE unit}$: it denotes a with only memory events.
As described in Section <ref>,
the final step of the second stage of modeling our programs  can use a handler for the memory events to obtain a computation in the state monad of type stateT mem (ctree voidE) unit.

§.§ Equational theory

The model described in Section <ref> allows us to derive some
program equivalences at source-level w.r.t. weak bisimilarity of their models.
For example, the following programs all just run $c$, though some of them first perform
some “invisible” steps related to concurrency (Lang.v331):

\[
\ssembra{\cfork {c} {\cskip}} \wbisim
\ssembra{\cseq{\cyield}{c}} \wbisim
\ssembra{c}
\]

We use weak rather than strong bisimilarity

since $\schedule$ can introduce stepping branches when interpreting the two concurrency events.
We emphasize that these equations are not compositional, they only hold in the absence of additional concurrent threads, hence why behaves as a no op: the monadic equivalence we obtain is a congruence for the source language after the first stage of interpretation, but not after the second stage.

Other equations, especially ones that make use of multiple threads in nontrivial
ways, rely on the stability of $\schedule$ under :

If the delayed branches of every element of vectors $v_n$ and $w_n$ have arity less than 2, and the elements of both vectors are strongly bisimilar up to a permutation $\rho$, then $\schedule~v_n~\SOME{i} \sbisim \schedule~w_n~\SOME{\rho~i}$.

The arity requirement is satisfied by all denotations of programs in this language.
This condition greatly simplifies the proof by constraining the shape that the
strongly bisimilar can take.

Lemma <ref> allows us to permute the thread pool, which is useful
in examples such as (Lang.v247):

\[
\ssembra{\cfork {c1} {(\cfork {c2} {\cskip})}} \wbisim
\ssembra{\cfork {c2} {(\cfork {c1} {\cskip})}}
\]

This program spawns two asynchronous threads then yields control to one of the two.
This equivalence captures the natural fact that it does not matter which thread is spawned first, since neither can run until both are spawned.

Furthermore, Lemma <ref> allows us to validate some simple optimizations that do not directly involve reasoning about concurrency or memory, such as (Lang.v363):

\begin{align*}
&\hfil\ssembra{\cfork {c1} {(\cfork {(\cwhile{\true}{\cyield})} {\cskip})}}\hfil\\
\wbisim\quad&\hfil\ssembra{\cfork {(\cseq{\cyield}{\cwhile{\true}{\cyield})} {(\cfork {c1} {\cskip})}}}\hfil
\end{align*}

This example is similar to the previous one, except that one of the spawned threads is a while loop, which we wish to unroll by one iteration.
Crucially, the loop and its unrolled form are strongly bisimilar, so this equivalence follows from Lemma <ref> just as in the previous example.
Other optimizations that can be done before interpreting events, such as
constant folding or dead code elimination, can be proven sound similarly.

Finally, equivalences involving memory operations are still valid as well (Lang.v443):

\[
\cfork {(\cassign{x}{2})} {(\cassign{x}{1})} \equiv
\cassign{x}{2}
\]

where $\equiv$ here refers to equivalence ($\wbisim$ in this case) after interpreting both concurrency and memory events.
This result follows from the result in Section <ref>, which allows us to transport equations made before interpreting state events into computations in the state monad after interpetation.

§ RELATED WORK

Since Milner's seminal work on  <cit.> and the $\pi$-calculus <cit.>,
process algebras have been the topic of a vast literature <cit.>.
We mention only a few parts of it that are most relevant to our work.
In the Coq realm, Lenglet et al. <cit.> have formalized HO$\pi$,
a minimal $\pi$-calculus, notably exhibiting the difficulty inherent to the
formal treatment of name extrusion.
Beyond its formalization, dealing with scope extrusion as part of a compositional semantics
is known to be a challenging problem <cit.>.
By restricting to in our case study, we have side-stepped this difficulty.
Foster et al. <cit.> formalize in Isabelle/HOL a semantics for CSP
and the Circus language using a variant implementation of , where
continuations to external events are partial functions. They, however, only model
deterministic processes, leaving support for nondeterministic ones to future
work. This paper introduces the tools to address that problem.
CSP has also been extensively studied by Brookes <cit.> by providing a
model based on the compositional construction of infinite sets of traces:
offers a complementary coinductive model to this more set-theoretic approach.
Furthermore, Brookes tackles questions of fairness, an avenue that we have not yet
explored in our setup.

Formal semantics for nondeterminism are especially relevant when dealing with
low-level concurrent semantics.  In shared-memory-based programming languages,
rather than message passing ones, concurrency gives rise to the additional
challenge of modeling their memory models, a topic that has received considerable
Understanding whether monadic approaches such as the one proposed in this paper
are viable to tackle such models vastly remains to be investigated.
Early suggestions that they may include  <cit.>
: the authors prove correct concurrent objects
implemented using , assuming a sequentially consistent model of shared
memory.  They relate the semantics to a trace-based one to reason about
refinement, something that we conjecture would not be necessary when starting
from .
Operationally specified memory models, in the style of which
increasingly relaxed models have been captured and sometimes formalized,
intuitively seem to be a better fit.
Major landmarks in this axis include the work by Sevcík
et al. on modeling TSO using a central synchronizing transition system linking
the program semantics to the memory model in the CompCertTSO
compiler <cit.>; or Kang et al.'s promising
semantics <cit.> that have captured large subsets of the C++11
concurrency model without introducing out-of-thin-air behaviors.
On the other side of the spectrum,
axiomatic models in the style of Alglave et al.'s <cit.>
framework appear less likely to transpose to our constructive setup.

Our model for cooperative multithreading is partially reminiscent of Abadi and Plotkin's work <cit.>:
they define a denotational semantics based on partial traces that they prove fully abstract, and satisfying
an algebra of stateful concurrency.
The main difference between the two approaches is that partial traces use the memory state explicitly to define the
composition of traces, where can express the semantics of a similar language independently of the memory model.
The formal model we describe here tackles a slightly different language than theirs, but we should
be able to adapt it reasonably easily to obtain a formalization of their work.
More recently, Din et al. <cit.> have suggested
a novel way to define semantics based on the composition of symbolic traces,
partially inspired by symbolic execution <cit.>.
They use it, in particular, to formalize actor languages, which rely on cooperative scheduling,
with a similar modularity as the one we achieve (orthogonal semantic features can be composed),
but not in a compositional way.

Our work brings proper support for nondeterminism to monadic interpreters in
. As with however, the tools we provide are just right to
conveniently build denotational models of first order languages, such as ,
but have difficulty retaining compositionality when dealing with higher-order languages.
In contrast, on paper, game semantics has brought a variety of techniques lifting this limitation.
In particular in a concurrent setup, event structures have spawned a successful line of
work <cit.> from which inspiration could be drawn for further work on .

§ CONCLUSION AND PERSPECTIVES

We have introduced , a model for nondeterministic,
recursive, and impure programs in . Inspired by , we have introduced
two kinds of nondeterministic branching nodes, and designed a toolbox to reason
about these new computations.
In addition to the library presented in this paper, we have developed an enhanced
implementation (with heavier notations, but more expressive) supporting arbitrary
indexing of branches and heterogeneous bisimulations between .
We have illustrated the expressiveness of the framework through two significant case studies.
Both nonetheless offer avenues for further work, notably through an extension of to
name passing à la $\pi$-calculus, and to further extend the equational theory
for cooperative multithreading that we currently support.

The restriction imposed on handlers in Section <ref> suggests
another perspective: rather than requiring handlers to implement events in a
non-observable way, we could prevent the programs in Figure <ref>
from being bisimilar in the first place.
We conjecture that this could be achieved by tweaking the LTS so that
external events induce two steps: the question to the environment first, and the answer second,
resulting in a finer grained bisimilarity.
Whether such a finer bisimilarity would still allow us to equate all
the programs we want needs further investigation.

§.§ Acknowledgements

We are grateful to the anonymous reviewers for their in-depth comments that
helped both improve this paper, and open avenues of further work.
We thank Gabriel Radanne for providing assistance with TikZ.
Finally, we are most thankful to Damien Pous for developing the coinduction
library this formal development crucially relies on, and for the numerous
advice he provided us with.

§ ELIMINATION OF STEPPING BRANCHES: A PROOF SKETCH

Stepping nondeterministic branches can be eliminated (Misc/brSElim.v249)

\[\forall t,~\ilc{BrSElim}~t\sbisim t\]

We proceed by coinduction, with the natural candidate: $\{(\ilc{BrSElim}~ t, t)~\mid~t\ilc{ : ctree E X}\}$.
We then case-analyse on the structure of $t$, and
partially reduce a step of iteration in each case (formally, this reduction
relies on the eta-unfolding of unary_stepping_form, which only holds
with respect to , and hence is made possible by the validity of strong bisimulation up-to ).

* Case x: we can simply conclude by reflexivity (validity of ).

* Case ek: the left-hand-side is of the shape
$\triggernoparens{e}~\bindc \lambda x \Rightarrow \guard~(\ilc{BrSElim}~(k~x))$.
It rewrites to
$\Vis{e}{\lambda x \Rightarrow \guard~(\ilc{BrSElim}~(k~x))}$
from which we can use the structural rule
(Figure <ref>)
to step without having to explicitly consider each process stepping.
At this point, we can almost conclude by coinductive hypothesis, except for
the trailing on the left-hand side; however, we can simply eliminate
it by rewriting the equation $\guard~t \sbisim t$ ().

* Case nk: We need to play explicitly the game in both directions—taking the branch $x$ of the n node is the same as taking both $x$
in n and crossing the .
We then conclude by coinduction by simply swiping off a $\guard$ as
in the previous case ().

* Case nk: Things are more involved in this case. Indeed, the case
analysis on $t$ has exposed a bit of syntax, a n node, that appears
on both side of the equation. However, as highlighted in
Figure <ref>, processing these nodes does not
give access to the coinduction hypothesis.
Rather, we introduce auxiliary lemmas to capture the state of the trees that
correspond to the next state of the LTS: one to transport a step in
BrSElim to one in its argument, and one the other way around.

* [right=L1]
𝙱𝚛𝚂𝙴𝚕𝚒𝚖 tlu
∃t', tlt'u 𝙱𝚛𝚂𝙴𝚕𝚒𝚖 t'

*[Right=L2]tlu∃u', 𝙱𝚛𝚂𝙴𝚕𝚒𝚖 tlu'u' 𝙱𝚛𝚂𝙴𝚕𝚒𝚖 u

Each of these lemmas are proved by reinforcing them to structurally specify
the shape of the arguments with respect to , and then proceeding by induction on
the transition.
Once we have these lemmas at hand, the main proof is straightforward: we
transport a step in the function to its argument by L1, use the hypothesis of
bisimilarity to transport it to the argument on the other side of the game,
and transport it back to the function by L2, allowing us to
conclude by coinduction hypothesis.

§ A SEMANTIC REPLICATION OPERATOR IN CCS$^{\#}$

For completeness, we provide below the denotational model of the $\sbang$ operator. The principles of this definition has been provided in the body of the article. Recall that we use an auxiliary operator $\sparabang {} {}$ to ensure syntactically that the coinductive definition is well-guarded.

p p p

p q F  p  q  ·

(p'p  F q p' )

(q'q  F p q')

(p'pq'q F p' q')

(q'qq”q F q' q”)

F q   (nk) n(λi ·F  (k i) q)

F q  (ek) e(λi ·F  (k i) q)

F p  (nk) n(λi ·F  (p k i) q )

F p  (ek) e(λi ·F  (p k i) q)

F  r r' {

·F  (k ()k' ()) q         if  ∃a.  r=(act  a)k r'=(act a̅)k'

F  r r' {

·F  (p k ()k' ()) q     if  ∃a.   r=(act  a)kr'=(act a̅)k'

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Abadi and PlotkinAbadi and Plotkin2010]
authorpersonMartín Abadi and
personGordon D Plotkin. year2010.
A model of cooperative threads.
journalLogical Methods in Computer Science
volume6, number4 (year2010),

<https://doi.org/10.2168/LMCS-6 (4:2) 2010>

[Abramsky and MellièsAbramsky and
authorpersonSampson Abramsky and
personPaul-Andreé Melliès.
Concurrent Games and Full Completeness. In
booktitleProceedings of the 14th Annual ACM/IEEE Symposium
on Logic in Computer Science. publisherIEEE Computer Society

[Alglave, Deacon, Grisenthwaite, Hacquard, and
MarangetAlglave et al2021]
authorpersonJade Alglave, personWill
Deacon, personRichard Grisenthwaite, personAntoine
Hacquard, and personLuc Maranget.
Armed Cats: Formal Concurrency Modelling at Arm.
journalACM Trans. Program. Lang. Syst.
volume43, number2 (year2021),

[Alglave, Maranget, and TautschnigAlglave
et al2014]
authorpersonJade Alglave, personLuc
Maranget, and personMichael Tautschnig.
Herding cats: modelling, simulation, testing, and
data-mining for weak memory. In booktitleACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI '14,
Edinburgh, United Kingdom - June 09 - 11, 2014,
editorpersonMichael F. P. O'Boyle and
personKeshav Pingali (Eds.). publisherACM,

[Altenkirch, Danielsson, and KrausAltenkirch
et al2017]
authorpersonThorsten Altenkirch,
personNils Anders Danielsson, and personNicolai
Kraus. year2017.
Partiality, Revisited. In
booktitleFoundations of Software Science and Computation
Structures, editorpersonJavier Esparza and
personAndrzej S. Murawski (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

[Bergstra, Ponse, and SmolkaBergstra
et al2001]
editorpersonJ.A. Bergstra, personA. Ponse,
and personS.A. Smolka (Eds.). year2001.
booktitleHandbook of Process Algebra.
publisherElsevier Science.

[Bloom, Istrail, and MeyerBloom
et al1988]
authorpersonB. Bloom, personS. Istrail,
and personA. R. Meyer. year1988.
Bisimulation Can't Be Traced. In
booktitleProceedings of the 15th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (San Diego, California,
USA) (seriesPOPL '88). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

[Brandauer, Castegren, Clarke,
Fernandez-Reyes, Johnsen, Pun, Tarifa, Wrigstad, and YangBrandauer
et al2015]
authorpersonStephan Brandauer, personElias
Castegren, personDave Clarke, personKiko
Fernandez-Reyes, personEinar Broch Johnsen,
personKa I Pun, personSilvia Lizeth Tapia Tarifa,
personTobias Wrigstad, and personAlbert Mingkun
Yang. year2015.
Parallel Objects for Multicores: A Glimpse at the
Parallel Language Encore. In booktitleFormal Methods for
Multicore Programming - 15th International School on Formal Methods for the
Design of Computer, Communication, and Software Systems, SFM 2015,
Bertinoro, Italy, June 15-19, 2015, Advanced Lectures
(seriesLecture Notes in Computer Science,
Vol. volume9104), editorpersonMarco
Bernardo and personEinar Broch Johnsen (Eds.).
publisherSpringer, pages1–56.

authorpersonStephen D. Brookes.
Traces, Pomsets, Fairness and Full Abstraction for
Communicating Processes. In booktitleProc. 13th Intl.  Conf. on Concurrency Theory (CONCUR 2002) (seriesLNCS,
Vol. volume2421), editorpersonLubos
Brim, personPetr Jancar, personMojmír
Kretínský, and personAntonín Kucera
(Eds.). publisherSpringer, addressBerlin Heidelberg,

authorpersonVenanzio Capretta.
General Recursion via Coinductive Types.
journalLogical Methods in Computer Science
volume1, number2 (year2005),

[Castellan, Clairambault, Rideau, and
WinskelCastellan et al2017]
authorpersonSimon Castellan, personPierre
Clairambault, personSilvain Rideau, and personGlynn
Winskel. year2017.
Games and Strategies as Event Structures.
journalLog. Methods Comput. Sci.
volume13, number3 (year2017).

[Crafa, Varacca, and YoshidaCrafa
et al2012]
authorpersonSilvia Crafa, personDaniele
Varacca, and personNobuko Yoshida.
Event structure semantics of parallel extrusion in
the pi-calculus. In booktitleLecture Notes in Computer
Science (including subseries Lecture Notes in Artificial Intelligence and
Lecture Notes in Bioinformatics), Vol. volume7213 LNCS.

[Cristescu, Krivine, and VaraccaCristescu
et al2013]
authorpersonIoana Cristescu, personJean
Krivine, and personDaniele Varacca.
A Compositional Semantics for the Reversible
$\pi$-Calculus. In booktitleProceedings - Symposium on
Logic in Computer Science. pages388–397.

[Din, Hähnle, Johnsen, Pun, and
Tapia TarifaDin et al2017]
authorpersonCrystal Chang Din, personReiner
Hähnle, personEinar Broch Johnsen, personKa I.
Pun, and personSilvia Lizeth Tapia Tarifa.
Locally Abstract, Globally Concrete Semantics of
Concurrent Programming Languages. In booktitleAutomated
Reasoning with Analytic Tableaux and Related Methods,
editorpersonRenate A. Schmidt and
personCláudia Nalon (Eds.). publisherSpringer
International Publishing, addressCham, pages22–43.

[Din, Hähnle, Henrio, Johnsen, Pun, and
TarifaDin et al2022]
authorpersonCrystal Chang Din, personReiner
Hähnle, personLudovic Henrio, personEinar Broch
Johnsen, personViolet Ka I Pun, and personSilvia
Lizeth Tapia Tarifa. year2022.
titleLAGC Semantics of Concurrent Programming Languages.

[Foster, Hur, and WoodcockFoster
et al2021]
authorpersonSimon Foster, personChung-Kil
Hur, and personJim Woodcock. year2021.
Formally Verified Simulations of State-Rich
Processes Using Interaction Trees in Isabelle/HOL. In
booktitle32nd International Conference on Concurrency
Theory, CONCUR 2021, August 24-27, 2021, Virtual Conference
(seriesLIPIcs, Vol. volume203),
editorpersonSerge Haddad and
personDaniele Varacca (Eds.). publisherSchloss
Dagstuhl - Leibniz-Zentrum für Informatik,

authorpersonRobert Harper.
booktitlePractical Foundations for Programming
publisherCambridge University Press.

[Henrio, Madelaine, and ZhangHenrio
et al2016]
authorpersonLudovic Henrio, personEric
Madelaine, and personMin Zhang.
A Theory for the Composition of Concurrent
Processes. In booktitleFormal Techniques for Distributed
Objects, Components, and Systems, editorpersonElvira
Albert and personIvan Lanese (Eds.).
publisherSpringer International Publishing,
addressCham, pages175–194.

[Hur, Neis, Dreyer, and VafeiadisHur
et al2013]
authorpersonChung-Kil Hur, personGeorg
Neis, personDerek Dreyer, and personViktor
Vafeiadis. year2013.
The Power of Parameterization in Coinductive
Proof. In booktitleProceedings of the 40th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome,
Italy) (seriesPOPL '13). publisherACM,
addressNew York, NY, USA, pages193–206.

[Kang, Hur, Lahav, Vafeiadis, and DreyerKang
et al2017]
authorpersonJeehoon Kang, personChung-Kil
Hur, personOri Lahav, personViktor Vafeiadis, and
personDerek Dreyer. year2017.
A promising semantics for relaxed-memory
concurrency. In booktitleProceedings of the 44th ACM
SIGPLAN Symposium on Principles of Programming Languages, POPL 2017,
Paris, France, January 18-20, 2017,
editorpersonGiuseppe Castagna and
personAndrew D. Gordon (Eds.). publisherACM,

authorpersonJames C. King.
Symbolic Execution and Program Testing.
journalCommun. ACM volume19,
number7 (dateJuly year1976),

[Kiselyov and IshiiKiselyov and
authorpersonOleg Kiselyov and personHiromi
Ishii. year2015.
Freer monads, more extensible effects. In
booktitleProceedings of the 8th ACM SIGPLAN Symposium on
Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015.

[Koenig and ShaoKoenig and Shao2020]
authorpersonJérémie Koenig and
personZhong Shao. year2020.
Refinement-Based Game Semantics for Certified
Abstraction Layers. In booktitleProceedings of the 35th
Annual ACM/IEEE Symposium on Logic in Computer Science (Saarbrücken,
Germany) (seriesLICS '20). publisherAssociation
for Computing Machinery, addressNew York, NY, USA,

[Lampropoulos and PierceLampropoulos and
authorpersonLeonidas Lampropoulos and
personBenjamin C. Pierce. year2018.
booktitleQuickChick: Property-Based Testing in
publisherElectronic textbook.

[Lee, Cho, Podkopaev, Chakraborty, Hur, Lahav,
and VafeiadisLee et al2020]
authorpersonSung-Hwan Lee, personMinki
Cho, personAnton Podkopaev, personSoham Chakraborty,
personChung-Kil Hur, personOri Lahav, and
personViktor Vafeiadis. year2020.
Promising 2.0: global optimizations in relaxed
memory concurrency. In booktitleProceedings of the 41st
ACM SIGPLAN International Conference on Programming Language Design and
Implementation, PLDI 2020, London, UK, June 15-20, 2020,
editorpersonAlastair F. Donaldson and
personEmina Torlak (Eds.). publisherACM,

[Lenglet and SchmittLenglet and
authorpersonSergueï Lenglet and
personAlan Schmitt. year2018.
HO\(\pi\) in Coq. In
booktitleProceedings of the 7th ACM SIGPLAN
International Conference on Certified Programs and Proofs, CPP 2018, Los
Angeles, CA, USA, January 8-9, 2018,
editorpersonJune Andronick and
personAmy P. Felty (Eds.). publisherACM,

[Lesani, Xia, Kaseorg, Bell, Chlipala, Pierce,
and ZdancewicLesani et al2022]
authorpersonMohsen Lesani, personLi-yao
Xia, personAnders Kaseorg, personChristian J. Bell,
personAdam Chlipala, personBenjamin C. Pierce, and
personSteve Zdancewic. year2022.
C4: verified transactional objects.
journalProc. ACM Program. Lang.
volume6, numberOOPSLA (year2022),

[Letan, Régis-Gianas, Chifflier, and
HietLetan et al2018]
authorpersonThomas Letan, personYann
Régis-Gianas, personPierre Chifflier, and
personGuillaume Hiet. year2018.
Modular Verification of Programs with Effects and
Effect Handlers in Coq. In booktitleFormal Methods - 22nd
International Symposium, FM 2018, Held as Part of the Federated Logic
Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings.

[Maillard, Hritcu, Rivas, and
Van MuylderMaillard et al2020]
authorpersonKenji Maillard,
personCătălin Hritcu, personExequiel
Rivas, and personAntoine Van Muylder.
The next 700 Relational Program Logics.
journalProceedings of the ACM on Programming
Languages volume4, numberPOPL, Article
articleno4 (year2020), numpages33 pages.

[Melliès and MimramMelliès and
authorpersonPaul-André Melliès and
personSamuel Mimram. year2007.
Asynchronous Games: Innocence Without Alternation.
In booktitleCONCUR 2007 – Concurrency Theory,
editorpersonLuís Caires and
personVasco T. Vasconcelos (Eds.). publisherSpringer
Berlin Heidelberg, addressBerlin, Heidelberg,

authorpersonR. Milner.
booktitleCommunication and Concurrency.
publisherPrentice-Hall, Inc., addressUSA.

authorpersonRobin Milner.
booktitleCommunication and Concurrency.
publisherPrentice-Hall, Inc., addressUSA.

[Milner, Parrow, and WalkerMilner
et al1992]
authorpersonRobin Milner, personJoachim
Parrow, and personDavid Walker.
A calculus of mobile processes, I.
journalInformation and Computation
volume100, number1 (year1992),

[Oliveira Vale, Melliès, Shao, Koenig, and
StefanescoOliveira Vale et al2022]
authorpersonArthur Oliveira Vale,
personPaul-André Melliès, personZhong Shao,
personJérémie Koenig, and personLéo
Stefanesco. year2022.
Layered and Object-Based Game Semantics.
journalProc. ACM Program. Lang.
volume6, numberPOPL, Article articleno42
(datejan year2022), numpages32 pages.

authorpersonDamien Pous.
Complete Lattices and Up-To Techniques. In
booktitleProgramming Languages and Systems,
editorpersonZhong Shao (Ed.).
publisherSpringer Berlin Heidelberg, addressBerlin,
Heidelberg, pages351–366.

authorpersonDamien Pous.
Coinduction All the Way Up. In
booktitleProceedings of the 31st Annual ACM/IEEE Symposium
on Logic in Computer Science (New York, NY, USA)
(seriesLICS '16). publisherAssociation for
Computing Machinery, addressNew York, NY, USA,

authorpersonDamien Pous.
booktitleThe coq-coinduction library.

authorpersonDamien Pous.
booktitleThe coq-coinduction library: examples.

[Rideau and WinskelRideau and
authorpersonSilvain Rideau and personGlynn
Winskel. year2011.
Concurrent Strategies. In
booktitleProceedings of the 26th Annual IEEE Symposium on
Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario,
Canada. publisherIEEE Computer Society,

authorpersonDavide Sangiorgi.
On the bisimulation proof method.
journalMathematical Structures in Computer Science
volume8, number5 (year1998),

[Sangiorgi and RuttenSangiorgi and
authorpersonDavide Sangiorgi and personJan
Rutten. year2012.
booktitleAdvanced Topics in Bisimulation and
Coinduction (edition2nd ed.).
publisherCambridge University Press,

[Sangiorgi and WalkerSangiorgi and
authorpersonDavide Sangiorgi and
personDavid Walker. year2001.
booktitleThe $\pi$-calculus (edition1st
publisherCambridge University Press,

[Sevcík, Vafeiadis, Nardelli,
Jagannathan, and SewellSevcík et al2013]
authorpersonJaroslav Sevcík,
personViktor Vafeiadis, personFrancesco Zappa
Nardelli, personSuresh Jagannathan, and personPeter
Sewell. year2013.
CompCertTSO: A Verified Compiler for
Relaxed-Memory Concurrency.
journalJ. ACM volume60,
number3 (year2013), pages22:1–22:50.

authorpersonM.B. Smyth.
Powerdomains. In
booktitleMathematical Foundations of Computer Science
(seriesLecture Notes in Computer Science,
Vol. volume4). publisherSpringer.

authorpersonThe Coq Development Team.
booktitleThe Coq Proof Assistant.

[Xia, Zakowski, He, Hur, Malecha, Pierce, and
ZdancewicXia et al2020]
authorpersonLi-yao Xia, personYannick
Zakowski, personPaul He, personChung-Kil Hur,
personGregory Malecha, personBenjamin C. Pierce,
and personSteve Zdancewic. year2020.
Interaction Trees.
journalProceedings of the ACM on Programming
Languages volume4, numberPOPL

[Yoon, Zakowski, and ZdancewicYoon
et al2022a]
authorpersonIrene Yoon, personYannick
Zakowski, and personSteve Zdancewic.
Formal Reasoning About Layered Monadic
journalProceedings of the ACM on Programming
Languages volume6, numberICFP

[Yoon, Zakowski, and ZdancewicYoon
et al2022b]
authorpersonIrene Yoon, personYannick
Zakowski, and personSteve Zdancewic.
Formal reasoning about layered monadic
journalProc. ACM Program. Lang.
volume6, numberICFP (year2022),

[Zakowski, Beck, Yoon, Zaichuk, Zaliva, and
ZdancewicZakowski et al2021]
authorpersonYannick Zakowski, personCalvin
Beck, personIrene Yoon, personIlia Zaichuk,
personVadim Zaliva, and personSteve Zdancewic.
Modular, Compositional, and Executable Formal
Semantics for LLVM IR.
journalProc. ACM Program. Lang.
volume5, numberICFP, Article articleno67
(dateaug year2021), numpages30 pages.

[Zakowski, He, Hur, and ZdancewicZakowski
et al2020]
authorpersonYannick Zakowski, personPaul
He, personChung-Kil Hur, and personSteve
Zdancewic. year2020.
An Equational Theory for Weak Bisimulation via
Generalized Parameterized Coinduction. In
booktitleProceedings of the 9th ACM SIGPLAN International
Conference on Certified Programs and Proofs (CPP).