# A Domain-Theoretic Framework for Composing Effectful Programs and Their Equations

David Nowak, Vlad Rusu

► To cite this version:

David Nowak, Vlad Rusu. A Domain-Theoretic Framework for Composing Effectful Programs and Their Equations. 2025. hal-05387384

HAL Id: hal-05387384

https://inria.hal.science/hal-05387384v1

Preprint submitted on 28 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# A Domain-Theoretic Framework for Composing Effectful Programs and Their Equations

David Nowak

Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France

Vlad Rusu

Univ. Lille, Inria, CNRS, Centrale Lille, UMR 9189 CRISTAL, F-59000 Lille, France

## Abstract

Interaction trees are a uniform compositional framework for representing effectful and potentially non-terminating computations. We develop a domain-theoretic formalization of interaction trees in the Rocq prover that handles (co)recursion and divergence naturally. We show that coproducts of interaction trees exist, allowing the modular combination of effect signatures, and that the equations defining each individual effect are seamlessly integrated through this structure. This enables modular equational reasoning for programs combining multiple effects. To illustrate the expressiveness of our approach, we verify the correctness of a stateful probabilistic computation and prove the equivalence between two programs whose termination depends on a mathematical conjecture.

**2012 ACM Subject Classification** Logic and verification - Equational reasoning

**Keywords and phrases** Interaction Trees; Domain Theory; Monad; Program Equivalence

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.2016.23

## 1 Introduction

Modern programming languages must account for computations involving effects such as mutable state, exceptions, nondeterminism, input/output, and continuations. Designing principled and compositional frameworks to reason about such effects has long been a central problem in programming language theory. A major breakthrough came from category theory, where monads emerged as a unifying abstraction for structuring computations with effects. Eugenio Moggi showed that monads offer a categorical semantics for effectful computation, bridging the gap between pure mathematical structure and programming practice [18, 20]. Philip Wadler later demonstrated how Moggi's insight could be applied concretely in the Haskell programming language [25].

Following this insight, language designers (especially within the Haskell community) began using monads to structure a wide range of computational effects. However, while monads neatly capture individual effects, it is not immediately clear how to combine monads to represent interacting effects. Several approaches have been proposed to address this composition problem.

One classical approach relies on distributive laws [7], which are natural transformations satisfying coherence conditions ensuring that the composite of two monads is itself a monad. Although elegant in theory, such distributive laws are often difficult or impossible to construct in practice, as they require highly specific interactions between effects.

In practice, particularly in Haskell, a more operational approach was developed through monad transformers [19]. A monad transformer extends an existing monad with an additional effect, producing a new monad. Despite their practicality, transformers do not always exist for every pair of effects, and their definitions appear to be ad hoc.

A more systematic and principled construction is provided by coproducts in the category of monads [17]. Categorically, a coproduct combines two structures in the most general way possible, preserving the behavior of each of them, without imposing additional interactions. It yields a monad that supports both effects in a modular way. Unfortunately, coproducts are not guaranteed to exist for all monads, and can be difficult to construct even when they exist. By restricting one's attention to *free monads*, however, the situation simplifies considerably: coproducts of free monads always exist and

<figure><img src="image_2.png" /></figure>

© David Nowak and Vlad Rusu;
licensed under Creative Commons License CC-BY 4.0

42nd Conference on Very Important Topics (CVIT 2016).

Editors: John Q. Open and Joan R. Acces; Article No. 23; pp. 23:1–23:23

<figure><img src="image_3.png" /></figure>

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

their construction is straightforward [24]. A free monad corresponds to a signature of operations and
represents all terms that can be formed from these operations without interpretation. Mathematically,
it freely adds monad structure to a functor (including its action on morphisms). And the coproduct of
two free monads is simply the free monad on the sum of their generating functors.

While free monads can easily be defined in Haskell, their standard inductive definition cannot be
transferred to Rocq, as it violates *strict positivity*, which, in turn, compromises logical consistency.
To circumvent this limitation, one can adopt *freer monads* which preserve positivity while expressing
the same idea: computations constructed from abstract operations [12]. Unlike free monads, freer
monads require only the object-level mapping of a signature and not the full functorial action. As
with free monads, coproducts of freer monads always exist and are straightforward to construct: the
coproduct of two freer monads is simply the freer monad over the sum of their operation signatures.

*Interaction-tree monads* [27] are a coinductive generalization of freer monads. They enable the representation of possibly infinite effectful computations. Each node of an interaction tree represents either a pure value, an effectful operation with a continuation, or a silent steps to insure the *productiveness* of corecursive computations. In this sense, interaction trees extend freer monads with coinduction, preserving modularity and compositionality while also supporting infinite behaviors, concurrency, and interaction with external environments. This makes them a powerful foundation for verified semantics, interpreters, and interactive systems in proof assistants such as Rocq [13, 21]. More recently, the choice-tree monad was introduced [8]. It is a coinductive monad that extends interaction trees with native support for nondeterministic branching, enabling the direct representation and equational reasoning about nondeterministic, recursive, and impure programs in Rocq.

In this paper we present a novel formalization of interaction trees in Rocq. Our approach is grounded in domain theory, which enables us to describe possibly non-terminating computations without relying on silent steps for productiveness. Moreover, our formalization supports coproducts and modular equational reasoning for programs that combine multiple effects: the equations defining each individual effect are seamlessly integrated through the coproduct structure of interaction trees. We illustrate the expressiveness of our framework by proving the correctness of a possibly non-terminating, stateful probabilistic program, and by establishing the equivalence between two programs encoding the Syracuse sequence, whose termination depends on an open mathematical conjecture.

74

Related Work

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

The FreeSpec framework [15, 16] offers a principled approach to the modular verification of effectful
programs in Rocq. It models computations as programs built using a freer monad, where each effectful
request is handled by an operational semantics describing how the system state evolves. This design
works well for deterministic effects, in which each request produces a single, well-defined result
and a uniquely determined successor state. However, extending FreeSpec to nondeterministic or
probabilistic effects introduces additional complexity. In such settings, an effect may yield a set
or distribution of possible outcomes, and the simple automaton-style operational semantics used
by FreeSpec is no longer sufficient. Properly capturing probabilistic behavior would require a
generalized probabilistic automaton or stochastic transition system, which is not supported in the
original framework. In contrast, our approach builds on the interaction-tree monad [27], a coinductive
generalization of freer monads that naturally accommodates possibly infinite executions. Rather
than giving an explicit operational semantics and reasoning through pre- and post-conditions, we
specify effects directly by equations describing the laws they satisfy, and we reason about programs
equationally within the monadic structure. The equational style substantially simplifies reasoning
and unifies the handling of diverse effects. Furthermore, effect composition in our framework is
achieved through the coproduct of effect signatures. Each individual effect is specified independently
by its equations, and, when composed, the equations are automatically integrated via the coproduct
structure of the interaction-tree monad. This modularity ensures that new effects can be added without reengineering existing proofs. As a result, our approach provides a clean, extensible foundation for reasoning about a broad spectrum of computational effects, including probabilistic and infinite behaviors, directly within Rocq, while retaining the algebraic nature of freer-monad-based designs.

While our work is closely related to existing developments on interaction trees [27], it differs both conceptually and technically in how it handles equality and (co)recursion. In the standard interaction-tree framework of [27], silent steps representing internal transitions induce a notion of weak bisimulation on interaction trees. The silent steps are also required for ensuring that corecursive definitions are guarded, and therefore accepted by Rocq's builtin productiveness checker. The consequence is that proofs typically require coinductive reasoning up to weak bisimulation.

In contrast, in our domain theoretical approach, bisimulation and equality are *provably* equivalent. Within this setting, we define an equivalence relation endowed with the appropriate congruence properties, allowing Rocq to perform rewriting directly. This removes the need for ad-hoc silent transitions and weak-bisimulation arguments, while preserving the ability to express infinite behaviors. A clear example of this appears in Section 4.2.2, where we define a *fold* function for providing possibly infinite interaction trees with a denotational semantics. This function produces values that are not in a Rocq builtin coinductive type, hence, it cannot be defined as a Rocq builtin corecursive function.

This semantic shift has important practical consequences for verification and proof automation. Because our equivalence relation is a congruence compatible with program constructs, standard Rocq rewriting tactics can be applied directly to simplify terms and discharge proof obligations, without requiring custom coinduction principles or up-to reasoning. The domain-theoretic interpretation enable us to prove in Rocq that all equations are sound with respect to the denotational semantics, so proofs can proceed purely equationally and compositionally. As a result, reasoning about effectful or infinite computations becomes tractable and amenable to automation: complex behavioral properties can be established through straightforward algebraic rewrites rather than elaborate weak-bisimulation arguments.

While our work shares the goal of enabling equational reasoning about monadic effectful programs with the Monae library [2, 3, 4], following the approach advocated by Gibbons and Hinze [9], our framework differs in both representation and abstraction. In Monae, effects are abstracted through type-class-like interfaces (implemented via mixins and canonical structures) and specified by equational laws. In contrast, our interaction-tree monads provide a mathematical replacement for these interfaces, offering a uniform and compositional representation of effectful components as coinductive interaction trees. The interaction-tree framework naturally supports complex scenarios, such as combining interaction-tree monads (to model components whose implementation is unknown) with standard monads (to model fully implemented programs). For example, a state monad transformer can be layered on top of a probabilistic interaction-tree monad to represent a stateful program that interacts with a probabilistic component. This illustrates how our approach internalizes and formalizes effect abstraction in a fully equational setting, achieving with interaction-tree monads what Monae accomplishes through type-class-like machinery.

Contextual equivalence for polymorphic languages with recursion and generic effects is studied by [10] who characterized it using logical relations. In [14], the authors develop an abstract account of applicative bisimilarity for an untyped lambda calculus with generic algebraic effects and prove that it is contained in contextual equivalence. In [22], a simply-typed language with recursion and generic algebraic effects is presented along with a modal logic for expressing program behavior. This logic induces a notion of logical equivalence that is sound with respect to contextual equivalence. These works represent just a few choices from a substantial and growing body of literature on program equivalence for effectful languages.
139

140

141

142

143

144

145

146

147

148

149

150

151

**Outline.** Section 2 provides the necessary background on domain theory, focusing on key notions: Complete Partial Orders (CPOs), continuous functions, and fixpoint theorems for defining (co)recursive functions and coinductive reasoning. Building on this foundation, Section 3 introduces CPO-monads, a monadic structure where the sequencing of actions is a continuous function. Concrete examples of CPO-monads are presented: continuation, state (transformer), and probability. Section 4 then examines the specific case of the interaction-tree CPO-monad and its associated equational reasoning techniques. Section 5 constructs the coproduct of interaction-tree monads by combining their effect signatures and shows how their equational theories can be combined as well. We illustrate these concepts with detailed examples in Section 6 and present our conclusions in Section 7. An Appendix provides details about a domain-theoretical construction called completion which serves as a replacement of Rocq's coinductive types, and which we use for defining interaction trees.

A complete implementation in the Rocq proof assistant is available at:

https://tinyurl.com/itreedomain.

152

153

154

155

The paper itself is written using conventional mathematical notation. This serves two purposes: first, it enhances readability, making the material accessible to a broader audience without expertise in Rocq or dependent type theory; and second, it underscores the generality of our method, showing that the techniques are not tied to a particular system and could be adapted to other proof assistants.

## 2 Background: Elements of Domain Theory

156

157

158

This section reviews the necessary background on domain theory, drawing from standard textbooks [5, 23, 26]. Our Rocq implementation formalizes a superset of the results presented hereafter.

### 2.1 Order relations

159

A partially-ordered set (poset) is a pair $(C, \leq)$ consisting of a set $C$ and a partial order $\leq$ on $C$.

160

161

A set $S \subseteq C$ is *directed* if $S \neq \emptyset$ and for all $x, y \in S$ there exists $z \in S$ such that $x, y \leq z$.

The least upper bound of a set $S$ is denoted by $lub S$. A directed complete partial order (DCPO) is a poset $(C, \leq)$ with the additional property that each directed set $S \subseteq C$ has a least upper bound.

162

163

164

A pointed partial order (PPO) is a triple $(C, \leq, \perp)$ where $(C, \leq)$ is a poset and $\perp \in C$ is the least element, i.e., $\perp \leq c$ for all $c \in C$. A complete partial order (CPO) is a DCPO that is also a PPO.

165

166

167

168

In a DCPO $(C, \leq)$, an element $c^\circ$ is *compact* if for all directed $S \subseteq C$, if $c^\circ \leq lub S$ then there exists $c \in S$ such that $c^\circ \leq c$. We denote by $C^\circ$ the set of compacts of $(C, \leq)$ and by $\leq^\circ$ the restriction of $\leq$ to $C^\circ$. We call $(C^\circ, \leq^\circ)$ the *poset of compacts* of $(C, \leq)$.

We denote by $C_c^\circ$ the set of compacts less or equal to $c$, i.e., $C_c^\circ := \{c^\circ \in C^\circ \mid c^\circ \leq c\}$.

169

170

171

Compact elements are essential in algebraic DCPOs (ADCPOs), which are DCPOs with the additional property that for all $c \in C$, the set $C_c^\circ$ is directed and $c = lub C_c^\circ$.

Algebraic CPOs (ACPOs) are the CPOs that are algebraic when seen as DCPOs.

172

173

These order relations are meant to be interpreted as *definition* orders: $x \leq y$ means that $x$ is at most as defined as $y$; $\perp$ is interpreted as undefined, maximal values are interpreted as being fully defined, and values that are neither undefined nor fully defined are partially defined.

174

175

176

A flat PPO is such that its elements are either undefined ($\perp$) or fully defined.

### 2.2 Closure

177

178

These orders are closed under Cartesian product and exponentiation.

Consider a set $J$ and a $J$-indexed set of sets $\{C_j \mid j \in J\}$. Their generalized Cartesian product $C := \prod_{j \in J} C_j$ is the set of functions $\{c : J \to \bigcup_{j \in C} C_j \mid \forall j. (c_j) \in C_j\}$.

179

180

181

If $j = \{0, 1\}$ one obtains the usual Cartesian product, denoted by $C_0 \times C_1$.
If all the sets $C_j$ are identical copies of some set $C$, then $\Pi_{j \in J} C_j$ coincides with $J \to C$. In this case the product is an exponentiation<fnref n="1" />.

182

183

If each $C_j$ has a partial order $\leq_j$, the pointwise order on $C$, defined by $c \leq c'$ iff for all $j \in J$, $c_j \leq \bar{c}'$ is a partial order as well.

184

185

If all the $(C_j, \leq_j)$ are DCPOs then $(C, \leq)$ is a DCPOs as well. If all the $(C_j, \leq_j, \perp_j)$ are CPOs (with $\perp_j \in C_j$) then $(C, \leq, \perp)$ with $\perp \triangleq \lambda j \to \perp_j$ is a CPO as well.

186

187

Finally, if all the $(C_j, \leq_j, \perp_j)$ are ACPOs then $(C, \leq, \perp)$ is an ACPO as well; its compacts are functions $c^\circ : J \to C_j^\circ$ with $c^\circ j \neq \perp_j$ for all but finitely many $j \in J$.

188

189

## 2.3 Completion

190

ADCPOs (resp. ACPOs) result from posets (resp. PPOs) by completion.

191

For a poset $(C, \leq^\circ)$, an ADCPO $(C, \leq)$ such that $(C, \leq^\circ)$ is isomorphic to the poset of compacts of $(C, \leq)$ is a completion of $(C, \leq^\circ)$. For a PPO $(C, \leq^\circ, \perp^\circ)$, a completion is an ACPO $(C, \leq, \perp)$ such that $(C, \leq)$ is a completion of $(C, \leq^\circ)$. Completions exist and are unique up to isomorphisms.

192

193

194

An interesting feature of completions is that they also apply to morphisms.

195

Morphisms of posets preserve poset structure, i.e., they are *monotonic* functions.

196

Morphisms of DCPOs preserve DCPO structure, i.e., they are *continuous*: if $(D, \leq)$ and $(C, \leq)$ are DCPOs, a function $f: D \to C$ is continuous when it is monotonic and for all directed $S \subseteq D$, $f(\text{lub } S) = \text{lub } (f S)$, where $f S \triangleq \{f x \mid x \in S\}$.

197

198

199

If $(D^\circ, \leq^\circ)$ and $(C^\circ, \leq^\circ)$ are posets with respective completions $(D, \leq)$ and $(C, \leq)$, then for any monotonic $f^\circ: D^\circ \to C^\circ$ there exists a unique continuous $f: D \to C$ such that $f d^\circ = f^\circ d^\circ$ for all compacts $d^\circ \in D^\circ$. We call $f$ the completion of $f^\circ$.

200

201

202

## 2.4 Kleene's Fixpoint Theorem

203

Consider a set $C$ and a function $F: C \to C$. Any $x \in C$ such that $F x = x$ is called a fixpoint of $F$.

204

If $F$ is monotonic and $(C, \leq, \perp)$ is a CPO then the sequence $(F^n)_{n \in \mathbb{N}}$ defined by $F^0 = \perp$ and for all $m \in \mathbb{N}$, $F^{m+1} = F(F^m)$ is monotonic; hence, $\{F^n \mid n \in \mathbb{N}\}$ is directed. Kleene's fixpoint theorem states that if, moreover $F: C \to C$ is continuous then $F$ has the least fixpoint $\mu F = \text{lub} \{F^n \mid n \in \mathbb{N}\}$.

205

206

207

This can be used for defining functions: by setting $C := A \to B$ with $A$ a set and $B$ a CPO, the pointwise order on $C$, as seen above, forms a CPO, and the least fixpoint of a continuous $F: (A \to B) \to (A \to B)$ defines a possibly partial function<fnref n="2" /> $\mu F: A \to B$. We use this technique for encoding partial functions in the total language of the Rocq prover. For example, the *bind* and *fold* functions on interaction trees are defined in this way.

208

209

210

211

212

The key condition in Kleene's fixpoint theorem is continuity. In practice, it may be difficult to prove this condition directly from its definition. Continuity of a large class of functions can, however, be proved by combining elementary continuity results [26]. These results include the continuity of constant and identity functions, of the composition of continuous functions, and of the unique completion of a monotonic function. Another result states that a function from a product DCPO $X \times Y$ to a DCPO $Z$ is continuous in its argument, say, $(x, y)$, if and only if it is continuous in $x$ and in $y$ separately. Yet another result, of our own making, gives an equivalent characterization of continuity, for the specific setting of functionals $F: (A \to B) \to (A \to B)$ with $A$ a set and $B$ a CPO: $F$ is continuous if and only if $F$ is monotonic and, for all directed sets $S \subseteq (A \to B)$, $F(\lambda (a : A) \to \text{lub} \{g a \mid g \in S\}) = \lambda (a : A) \to \text{lub} \{F g a \mid g \in S\}$. We call this characterization

213

214

215

216

217

218

219

220

221

222

<footnote n="1">¹ In the corner case $J = \emptyset$, $J \to C$ has exactly one element, the unique function from $\emptyset$ to $C$.</footnote>

<footnote n="2">² A function $f: A \to B$ is possibly partial if $f x = \perp$ for $x$ in some subset $C$ of $A$; if $C = \emptyset$ the function is total. Possibly partial functions include total ones. Hereafter we drop the "possibly" qualifier for possibly partial functions.</footnote>
223

224

225

*H-continuity.* *H-continuity* is easier to establish than plain continuity because the latter requires one to reason about *lubs* in the higher-order CPO *A* → *B*, while the former only uses *lubs* in the lower-order CPO *B*.

226

## 2.5 Knaster-Tarski's Fixpoint Theorem

227

228

229

230

231

232

233

234

235

236

237

238

239

Knaster-Tarski's fixpoint theorem gives conditions different from Kleene's fixpoint theorem for the existence of fixpoints. We are interested in greatest fixpoints in order to obtain coinductive objects.

A *complete upper lattice* is a poset ($L, \leq$) where *lub* $S$ exists for all $S \subseteq L$. A consequence of Knaster-Tarski's theorem says that if ($L, \leq$) is a complete upper lattice and $F : L \to L$ is monotonic, then $vF \triangleq lub\{x \in L | x \leq f x\}$ is the greatest fixpoint of $F$. The specialization of this result to the lattice of subsets of a set $Q$, i.e., $(2^Q, \subseteq)$, entails that any monotonic function $F : 2^Q \to 2^Q$ has the greatest fixpoint $vF \subseteq Q$. We say that $vF$ is *coinductively defined* by is *functional F*. The equation $vF = F(vF)$ is called the *unfolding equation of vF*. The fact that $vF$ is the greatest fixpoint of $F$, rewritten as *for all* $P \subseteq Q, P \subseteq F P$ *implies* $P \subseteq vF$, is called the *coinduction principle of vF*.

We use such principle to encode coinductive predicates and proofs in Rocq, as an alternative to the builtin coinduction of the proof assistant. The coinduction principle also enables reasoning over an alternative encoding of coinductive *types* whose construction is summarized in the Appendix. The resulting version of coinductive types is used ahead in the paper for defining interaction trees.

240

# 3 CPO-Monads

241

242

243

A *CPO-monad* is a monadic structure whose values are organized as a CPO. Hence CPO-monads contain an undefined value $⊥$ and may contain partially and/or fully defined values. All the monadic structures occurring in this paper, including interaction trees, are CPO-monads.

244

245

246

► **Definition 1.** A CPO-monad is a structure $(M, \text{ret}, \text{bind})$ where $M: \text{Set} \to \text{CPO}$ is a functor from sets to CPOs, and, for each set $X$ and $Y$, $\text{ret}_X: X \to MX$ and $\text{bind}_{X,Y}: MX \to (X \to MY) \to MY$ are functions such that, with the notation $do x \leftarrow m$; $m' \triangleq \text{bind}_{X,Y} m (\lambda x.m')$:

247

■ $\forall X Y (k : X \to M Y), \lambda m. \text{do } x \leftarrow m; k x \text{ is continuous as a function between } M X \text{ and } M Y$;

248

■ $\forall X Y (m : M X), \lambda k. \text{do } x \leftarrow m; k x \text{ is continuous as a function between } (Y \to M X)^3 \text{ and } M Y$.

249

■ `ret` and `bind` satisfy the standard monadic laws:

250

■ $\forall X (m : M X), \text{do } x \leftarrow m; \text{ret } x = m$

251

■ $\forall X Y (x : X)(f : X \to M Y), \text{do } x' \leftarrow \text{ret}_X x; f x' = f x$

252

■ $\forall X Y Z (m : M X)(f : X \to M Y)(g : Y \to M Z)$,

253

do $y \leftarrow (\text{do } x \leftarrow m; f x); g y = \text{do } x \leftarrow m; \text{do } y \leftarrow f x; g y$

254

255

256

257

258

► **Remark 2.** CPO-monads diverge from the usual definition of monads: their functors are not endofunctors, but functors from sets to CPOs<fnref n="4" />. Attempts to cast our definition in the proper categorical definition of monads, i.e., requiring endofunctors between CPOs, requires more implementation work (more complications due to dependent types, more continuity proofs, ...) without much practical benefit. Hence we choose the above hybrid definition of CPO-monads.

259

260

**Notation.** For sets $X$ and $Y$, $X + Y$ denotes their disjoint sum, with injections $\text{inl} : X \to X + Y$ and $\text{inr} : Y \to X + Y$. **1** denotes the unit set, with exactly one element, $\ast$.

<footnote n="3">³ here we use the fact that CPOs are closed under exponentiation with a set.</footnote>

<footnote n="4">⁴ the effect of the functor on morphisms: by the continuity of *bind* in its first argument, every function *f*: *X* → *Y* is mapped by the functor *M* to *M* *f* := *λm* ⇒ *do* *x* ← *m*; *ret* (*f* *x*), which a continuous function from *M* *X* to *M* *Y*.</footnote>
► **Example 3.** Before we give examples of CPO-monads we show how a notion of while-loop can be defined at an abstract level, independently of any programming language.

We start by defining an *iterator*. For any set $Y$, consider the functional $F_Y : M(\mathbf{1} + Y) \to MY \to MY$ where:

$$F_Y m \text{ rec} = \text{do } r \leftarrow m; \begin{cases} \text{rec} & \text{if } r = \text{inl} * \\ \text{ret y} & \text{if } r = \text{inr y} \end{cases}$$

One can prove using the techniques presented in Section 2.4 that for all $Y$ and $m \in M(\mathbf{1} + Y)$, $(F_Y m) : MY \to MY$ is continuous. By Kleene's fixpoint theorem we obtain the fixpoint equation

$$\mu(F_Y m) = \text{do } r \leftarrow m; \begin{cases} \mu(F_Y m) & \text{if } r = \text{inl} * \\ \text{ret y} & \text{if } r = \text{inr y} \end{cases}$$

In particular a while-loop is defined as least fixpoint of $F_Y m$ for certain $Y, m$, and satisfies the equation

$$\text{while } \text{cond body} = \text{do } b \leftarrow \text{cond}; \begin{cases} \text{body}; & \text{while } \text{cond body} \quad \text{if } b = \text{true} \\ \text{ret } * & \text{if } b = \text{false} \end{cases}$$

We now give some examples of CPO-monads that we use hereafter in the paper.

► **Example 4 (The option CPO-monad).** This monad consists of:

the functor *option* maps any set $X$ to the flat CPO $X \cup \{\perp\}^5$;

for all sets $X$ and $x \in X$, $\text{ret } x = x$;

do $x \leftarrow m$; $f x$ is $\perp$ if $x = \perp$ and $f x$ otherwise.

The continuity requirements of a CPO-monad are proved using the techniques from Section 2.4.

► **Example 5 (The continuation CPO-monad).** The continuation monad (*Cont*, *ret*, *bind*) models the concept of “the rest of the computation” (the so-called continuation). The continuation monad parameterized by a CPO $R$ is defined as follows:

the functor $\text{Cont}_R$ maps each set $X$ to the CPO of continuous functions from $X \to R$ to $R$ that take as input a continuation and yields a final result. Intuitively, they encapsulate a value not as a concrete result, but as a suspended computation awaiting its future.

$\text{ret } x$ is defined as $\lambda k. k x$. It injects a value $x$ into the continuation monad. Conceptually, it creates a suspended computation that, when resumed by a continuation $k$, amounts to applying $k$ to $x$.

do $x \leftarrow m$; $f x$ is defined as $\lambda k. m (\lambda x. f x k)$. It enables the composition of two continuation-based computations where the second is dependent on the result of the first. The operation do $x \leftarrow m$; $f x$ can be understood as follows: it takes an initial computation $m$ and a function $f$ that will generate a subsequent computation based on $m$'s output. The result of this is a composite continuation. When this composite continuation is invoked with a final continuation $k$, it first executes $m$, but not with the final continuation $k$. Instead, it executes $m$ with a new intermediate continuation. This intermediate continuation is a function that takes the future result $x$ from $m$, applies $f$ to it to generate the next computation $f x$, and then launches $f x$ with the original final continuation $k$.

We discharge the continuity requirements of CPO-monads by applying the techniques from Section 2.4.

► **Example 6 (The probability CPO-monad).** The probability CPO-monad is instantiated from the continuation CPO-monad by fixing the result type $R$ to be the CPO $[0, 1]$ under its standard linear order [6]. We equip this monad with a primitive *flip*, representing a Bernoulli trial with a

<footnote n="5">⁵ where $\perp \notin X$ is the least element in the CPO, and elements of $X$ are not comparable to each other</footnote>
290

291

292

293

294

295

296

certain success probability. This is realized by defining *flip* *p* as the continuation λk. *p* (*k* true) + (*1* − *p*) (*k* false). This definition computes the expected value of the continuation *k* by taking a weighted average of its application to *true* and *false*, thereby encoding the specified probability distribution. From this primitive, more complex probabilistic constructs can be derived. For instance, it is straightforward to define a choice function that selects between two monadic computations based on the outcome of a flip. Furthermore, one can construct a recursive function that induces a uniform distribution over a given list of values.

297

298

299

300

301

Next, we define the state CPO-monad transformer. A CPO-monad transformer is defined to augment an existing CPO-monad with a new effect, producing another CPO-monad. This structure also provides a method to lift operations from the original monad into the augmented one. For example, we shall be using the state monad transformer, presented below, in combination with the continuation monad from Example 6.

302

303

304

**► Example 7 (The state CPO-monad transformer).** Given a CPO-monad (*M*, *ret*<sub>*M*</sub>, *bind*<sub>*M*</sub>), the state CPO-monad transformer parameterized by a set *S* of states constructs a new CPO-monad (*State*<sub>*S*</sub><sup>*M*</sup>, *ret*, *bind*) as follows:

305

■ *State*<sub>*S*</sub><sup>*M*</sup> *X* maps a set *X* the the CPO *M*(*X* × *S*).

306

307

■ *ret* *x* is defined as λs. *ret*<sub>*M*</sub>(*x*, *s*). It produces a stateful computation that leaves the state unchanged and yields the value *x* inside the underlying monad *M*.

308

309

310

■ do *x* ← *m*; *f* *x* is defined as λs. do (*x*, *s*') ← *m* *s*; *f* *x* *s*'. This operation sequences two stateful computations, threading the state through both while remaining inside the context of the base monad *M*.

311

312

This CPO-monad transformer is equipped with two fundamental primitives, *get* and *put*, which provide access to the state:

313

314

315

■ The *get* primitive retrieves the current state. It is defined as λs. *ret*<sub>*M*</sub>(*s*, *s*). This operation takes a state *s* and returns a computation in *M* that produces the pair (*s*, *s*), thereby yielding the current state value while leaving the state itself unchanged.

316

317

318

319

■ The *put* *s*′ primitive updates the state to a new value *s*′. It is defined as λs. *ret*<sub>*M*</sub>(*∗*, *s*′). This operation ignores the incoming state *s* and returns a computation that produces the pair (*∗*, *s*′). This signifies that the operation’s result is the unit value *∗* (a placeholder indicating no meaningful result), and the state is updated to *s*′.

320

321

As usual, we discharge the continuity requirements of CPO monads by applying the techniques from Section 2.4.

322

323

324

325

By instantiating the state CPO-monad transformer parameterized by state-set *S* with the option monad we obtain the state-CPO monad over states *S*; its functor is *State*<sub>*S*</sub> : *X* → (*X* × *S*) ∪ {⊥}. Likewise, by instantiating the state CPO-monad transformer with the probability CPO-monad we obtain a CPO-monad combining state and probability.

326

4 Interaction Trees

327

We now focus on interaction trees: their definition and basic properties, and their monadic structure.

328

4.1 Interaction Trees: Definition and Basic Properties

329

330

We define interaction trees by means of *containers*; the details of the encoding are in the Appendix.
The encoding is transparent, hence the details can be skipped. What the user “sees” is the following.
► **Definition 8 (Interaction Trees).** Given a partial function $F : Set \to Set$ (called the effect signature) and a set $X$, the set $itree F X$ is coinductively defined as: for all $t \in itree F X$, $t = \perp$ or (exclusively) there exists a unique $x \in X$ such that $t = pure_X x$, or (exclusively) there exist unique $Y \in Set$, $fy \in F Y$, and $k : Y \to itree F X$ such that $t = impure_Y fy k$.

► **Remark 9.** We emphasize that the coinduction in Definition 8 is an artifact of our encoding. In particular, it is not the builtin coinduction of Rocq. The definition can be understood as follows: $itree F X$ is a set of labelled trees of arbitrary breadth and possibly infinite depth, whose leaves are either $\perp$ or $pure_X x$ for some $x \in X$, and nodes are of the form $impure_Y fy k$ for $Y \in Set$, where $fy \in F Y$ is the node's label and $k : Y \to itree F X$ defines the set of subtrees (of cardinality $|Y|$) of the node. Infinite depth is obtained by nesting the *impure* constructor a countably infinite number of times.

Interaction trees of a given effect signature are ordered according to the following relation:

► **Definition 10 (order).** For all $X \in Set$, the order relation $\leq \subseteq$ $itree F X \times itree F X$ is coinductively defined as follows: $t \leq_X t'$ iff either $t = \perp$, or $t = t' = pure_X x$ for some $x \in X$, or there exist $Y \in Set$, $fy \in F Y$, and $k, k' : Y \to itree F X$ such that $t = impure_Y fy k$, $t' = impure_Y fy k'$ and for all $y \in Y, (k, y) \leq (k', y)$.

► **Lemma 11.** With the order $\leq$ from Definition 13, $(itree F X, \leq, \perp)$ is an ACPO.

► **Remark 12.** The coinductive definition of order is based on a corollary to the Knaster-Tarski theorem (cf. section 2.5). Again, this is not the builtin coinduction of Rocq.

The reflexive closure of the $\leq$ defines a bisimulation relation on interaction trees:

► **Definition 13 (Bisimulation).** The bisimulation relation $\approx \subseteq$ $itree F X \times itree F X$ is defined by $t \approx t'$ iff $t \leq t'$ $\land$ $t' \leq t$.

► **Lemma 14.** Equality on interaction trees coincides with bisimulation: $t = t'$ iff $t \approx t'$.

In order to prove equality of interaction trees we use Lemma 14 together with the following one:

► **Lemma 15 (Coinduction Principle for Bisimulation).** Given $t, t' \in itree F X$, in order to prove $t \approx t'$ it is enough to find $R \subseteq$ $itree F X \times itree F X$ with $(t, t') \in R$ and prove that for all $(u, v) \in R$, $u = v = \perp$ or $u = v = pure X$ for some $x \in X$, or $u = impure_Y fy k$, $t' = impure_Y fy k'$ for some $Y \in Set$, $fy \in F Y$, and $k, k' : Y \to itree F X$, such that for all $y \in Y, ((k, y), (k', y)) \in R$.

We now give two examples of effect signatures for interaction trees that are used ahead in the paper. Remember that interaction trees contain but do not interpret their effects.

► **Example 16 (Probability effect signature).** The signature of probabilistic effects is defined by a partial function $Prob : Set \to Set$ defined only on Booleans: $Prob \mathbb{B} = \bigcup_{p \in \{0,1\}} \{Flip (p)\}$. This defines an interface for probabilistic computations: the only primitive effect is **Flip $p$** and represents a probabilistic choice. The interaction trees with effect signature $Prob$ can thus represent programs that make repeated probabilistic choices, branching according to the outcomes of these choices.

► **Example 17 (State effect signature).** The signature of state-manipulating effects over a set $S$ of states is defined by a partial function $State_S : Set \to Set$, defined only on the sets $S$ and $1$ by:

$$State_S S = \{\text{get}\}$$

$$State_S 1 = \bigcup_{s \in S} \{\text{put } s\}$$

This defines the interface for stateful computations. The corresponding interaction tree can thus represent programs that interact with a mutable state cell by reading from and writing to it over the course of their execution.
The following function takes an effect fy of type F Y turns it into an elementary interaction tree:

► **Definition 18 (Trigger).**

$$ \mathit{trigger} \ fy = \mathit{impure}_Y \ fy \ \mathit{pure}_Y. $$

Intuitively, *trigger* is the most basic way to inject a single, primitive effect into an interaction tree for the corresponding effect. It takes an uninterpreted effect *fy* (like **Flip p** or **get**) and wraps it into an interaction tree. The resulting tree is a single effect node whose immediate continuation is *pure*.

Interaction trees have one additional primitive: *fold*, which is mainly used for interpreting the effects contained in a tree and accumulating them into a single value. It is presented in the next section because its definition shares some features with the *bind* connector, part of the CPO monads structure of interaction trees.

## 4.2 Interaction Trees as CPO-monads

We now show that interaction trees are instances of CPO-monads (cf. Definition 1). We start by defining the *ret* and *bind* connectors and prove the continuity of *bind*. Specifically, *bind* is a corecursive function, defined as the least fixpoint of its continuous functional. The monad laws are proved using the coinduction principle for interaction trees (cf. Lemma 15). Thanks to the equivalence between equality and bisimulation from Lemma 14, the monad laws are Rocq equalities<fnref n="6" />.

Then, we define a *fold* function for interaction trees, also as the least fixpoint of its continuous functional, and prove its continuity. *fold* is used, among others, for traversing interaction trees while interpreting and accumulating the effects therein, which endows interaction trees with *denotations*.

The section continues with the definition of the coproduct and of equivalences for interaction trees. This enables us to prove program equivalences, illustrated on examples in the next section.

### 4.2.1 Ret, Bind, and Monadic Laws

For interaction trees parameterized by an effect signature $F : Set \to Set$ and a set $X$, we define the monadic elementary computation $\text{ret}_X : X \to \text{itree}_F X$ by $\text{ret}_X = \text{pure}_X$. For the sequencing of computations $\text{bind} : \text{itree}_F X \to (X \to \text{itree}_F Y) \to \text{itree}_F Y$, we first identify its expected properties:

for all $f : X \to \text{itree}_F Y, \text{bind} \perp f = \perp$;

for all $x \in X$ and $f : X \to \text{itree}_F Y, \text{bind} (\text{ret}_X x) f = f x$;

for all $Z \in Set, fz \in FZ, k : Z \to \text{itree}_F X, \text{and } f : X \to \text{itree}_F Y, \text{bind} (\text{impure}_Z fz k) f = \text{impure}_Z fz (\lambda z. \text{bind} (k z) f)$.

The first identity states that sequencing an undefined computation with anything produces an undefined computation; the second identity is one of the monad laws (left neutrality of *ret* w.r.t. *bind*); and the third identity defines *bind* in terms of itself. If interaction trees were defined using the builtin coinduction of Rocq, one could define *bind* using a Rocq corecursive function that amounts to stating the three above identities. But interaction trees are not defined using the coinduction of Rocq. Hence, in order to define *bind*, we use Kleene’s fixpoint theorem.

Since Kleene’s theorem can only define functions of one argument, but *bind* has two arguments, we shall first define its *uncurried* version $\widehat{bind} : (\text{itree}_F X) \times (X \to \text{itree}_F Y) \to \text{itree}_F Y$. The corresponding functional $\widehat{fbind}$ for effect signature $F$ and sets $X, Y$ is written using pseudocode in Figure 1. Its type is $((\text{itree}_F X) \times (X \to \text{itree}_F Y) \to \text{itree}_F Y) \to ((\text{itree}_F X) \times (X \to \text{itree}_F Y) \to \text{itree}_F Y)$. We note that the domain and codomain of $\widehat{fbind}$ are the same and are CPOs, because

<footnote n="6">⁶ This in contrast to [27], where monad laws only hold up to a certain *weak bisimulation*.</footnote>
interaction trees are (A)CPOs and CPOs are closed under exponentiation and product. We prove that $\widehat{fbind}$ is continuous by the techniques presented in Section 2.4. Then, Kleene's theorem ensures that $\widehat{fbind}$ has a least fixpoint, of type $(itree F X) \times (X \to itree F Y) \to itree F Y$. We call this least fixpoint $\widehat{bind}$.

408

409

410

411

412

413

By currying $\widehat{bind}$ we obtain the desired bind function, of the proper type. By expanding the fixpoint equation $\widehat{fbind} \widehat{bind} = \widehat{bind}$ we obtain the three identities from the beginning of this section.

$\widehat{fbind}(\phi : (itree F X) \times (X \to itree F Y) \to itree F Y) (p : itree F X \times (X \to itree F Y)) : itree F Y :=$
let $(m, f) = p$ in

case $m$ of

$\perp \Rightarrow \perp$

$\text{pure}_X x \Rightarrow f x$

$\text{impure}_Z \text{fz} k \Rightarrow \text{impure}_Z \text{fz} (\lambda z. \phi ((k z), f))$

end

■ **Figure 1** Functional $\widehat{fbind}$, for the uncurried $\widehat{bind}$.

414

415

In order to conform to Definition 1 of CPO-monads we still need to prove that $\widehat{bind}$ is continuous in both arguments, and that the monad laws hold.

416

417

- Proving that $\widehat{bind}$ is continuous in both arguments is equivalent, by a result given in Section 2.4, to proving that $\widehat{bind}$ is continuous in its single argument (a pair). We proceed as follows:

418

419

- We first prove that $\widehat{fbind}$ preserves continuity: if $\phi : (itree F X) \times (X \to itree F Y) \to itree F Y$ is continuous, then $\widehat{fbind} \phi : (itree F X) \times (X \to itree F Y) \to itree F Y$ is continuous as well;

420

421

- Then, we prove by induction over natural numbers that for all $n \in \mathbb{N}$, the $n$-th iteration of $\widehat{fbind}$ starting with a constant $\perp$ function, i.e., $\widehat{fbind}^{(n)}(\lambda_{\_} \Rightarrow \perp)$, is continuous;

422

423

424

- Finally, we note that the set $\{\widehat{fbind}^{(n)}(\lambda_{\_} \Rightarrow \perp) \mid n \in \mathbb{N}\}$ is directed, and use a result from domain theory stating that the *lub* (here, $\widehat{bind}$) of a directed set of continuous functions is a continuous function as well. This ensure that $\widehat{bind}$, and then $\widehat{bind}$, are continuous.

425

426

427

428

- for the monad laws: the fact that $\text{ret}$ is neutral to the left of $\widehat{bind}$ is already the second identity given at the beginning of the section. The two other laws - $\text{ret}$ is neutral to the right of $\widehat{bind}$, and $\widehat{bind}$ is associative - are stated as equalities, transformed thanks to Lemma 14 into bisimulations, and proved using the coinduction principle for bisimulation on interaction trees (Lemma 15).

429

### 4.2.2 Fold

430

431

432

Interaction trees have one additional primitive: *fold*, for traversing a tree and accumulating some function of its nodes into one value. This is used, in particular, for computing the accumulated effects encoded in a tree, which amounts to endowing interaction trees with a denotational semantics.

433

434

Since interaction trees can be partially defined (i.e., some leaves are $\perp$), their denotations can be partially defined as well. To account for such situations we let the return value of *fold* inhabit a CPO.

435

436

437

We first give the expected properties of the *fold* function, then define it using Kleene's fixpoint theorem. Given $F : \text{Set} \to \text{CPO}$ (the effect signature), a set $X$, a CPO $Y$, a function $f : X \to Y$, and a function $g_Z : FZ \to (Z \to Y) \to Y$ parameterized by a set $Z$, *fold* $f g_Z : itree F X \to Y$ is such that

438

- *fold* $f g_Z \perp = \perp$;

439

- *fold* $f g_Z (\text{pure}_X x) = f x$;

440

- *fold* $f g_Z (\text{impure}_Z \text{fz} k) = g_Z \text{fz} (\lambda z. \text{fold} (k z))$.

441

Consequently, the expected functional for *fold* is given in Figure 2.
```
ffold (f : X → Y) (g_Z : F Z → (Z → Y) → Y) (φ : itree F X → Y) (t : itree F X) : Y :=
    case t of
        ⊥ ⇒ ⊥
        pure_X x ⇒ f x
        impure_Z fz k ⇒ g_Z fz (λz. φ (k z))
    end
```

<caption>Figure 2 Functional for fold.</caption>

However, there is a catch. Proving that `ffold f g_Z : (itree F X → Y) → (itree F X → Y)` is continuous (as required by Kleene's fixpoint theorem) requires the hypothesis that for all $Z \in \mathcal{S}et$ and $fz : F Z, (g_Z fz) : (Z \to Y) \to Y$ is continuous as well. In the dependently-type setting of Rocq this amounts to adding an argument to `ffold`: a proof of continuity for $g_Z fz$. Here we omit the additional argument for the sake of readability. Using this additional hypothesis, the proof of continuity of `ffold f g_Z` is performed using the techniques shown in Section 2.4. By Kleene's fixpoint theorem, the least fixpoint of `(ffold f g_Z)` is `fold f g_Z`, which satisfies the requirements stated above for the `fold` function. Moreover, we prove that `fold f g_Z` is continuous as a function from the CPO `itree F X → Y` to itself, using the techniques described in Section 4.2.1 for the continuity of `bind`.

**Denotations for Interaction Trees.** We now give examples of using `fold` for giving denotations to interaction trees. This is achieved by calls of the form `fold ret g m`, which traverses the interaction tree `m` and applies the function `g` to each effect in `m`. The overall result is a value in a concrete monad, typically, one implementing the effect of `m`.

**► Example 19 (Denotation of the interaction-tree probability monad).** The denotation `g (Flip p)` into the probability monad (cf. Example 6) is $\lambda k. \text{do } b \leftarrow \text{flip } p; k b$. Intuitively, this explains how to handle a single flip effect in the context of the entire computation. The function `g` takes the effect `Flip p` and produces a probabilistic program that:

- First, performs a random flip of a biased coin (with probability `p`), binding the outcome `true` or `false` to the variable `b`.

- Then, resumes the rest of the computation `k`, passing this boolean result `b` to it.

In this way, `g` translates the abstract `Flip p` node into a concrete monadic action that the probability monad can execute.

**► Example 20 (Denotation of the interaction-tree state monad).** Given an underlying monad `M`, the denotations induced by the parameter `g` of `fold`, i.e., `g get` and `g (put s')` into the state monad transformer `StateT_S^M` (cf. Example 7) are given respectively by $\lambda k.k s s$ and $\lambda k.k * s'$. Intuitively, these definitions describe how to handle state operations:

- For `get`: The function `g` produces an action that takes the current state `s`. It then calls the function `k` with two arguments: first, the value `s` (so the rest of the computation can use it), and second, the state `s` again (leaving the state unchanged for the subsequent computation).

- For `put s'`: The function `g` produces an action that takes a new state `s'`. It then calls the function `k`, passing a dummy unit value `*` (since a `put` operation carries no meaningful result) and, crucially, updating the state to `s'` for all future operations.

In this way, `g` translates the abstract `get` and `put s'` effects into concrete state-passing actions.

## 4.3 Congruence for Equational Reasoning on Interaction Trees

We now turn to defining congruence relations for interaction trees. First, why does one need congruences in the first place - why is bisimulation (which, in the present case, coincides with
equality) not good enough? The reason is the very nature of interaction trees, as structures that sequence and combine effects but do not interpret them. The interpretation is the task of the *denotation* operation, which gives us an important criterion for a congruence to be *correct*: if two interaction trees are congruent, then that the two trees must have the same denotation.

Although we do not prove the converse (completeness), the relation is sufficiently powerful for proving the congruence of non-trivial programs (as will be illustrated in Section 6).

Our relation $\equiv$ is actually the union of a family of relations parameterized by an effect signature $F: Set \to Set$. Each relation $\equiv_F$ in the family is such that $\equiv_F \subseteq \bigcup_{X \in Set}(itreeF X) \times (itreeF X)$; that is, $\equiv_F$ relates trees in $itreeF X$, for all sets $X$. Each $\equiv_F$ is defined as the least relation satisfying the following constraints:

- first, $\equiv_F$ includes a base relation, specific to the effect signature $F$. Intuitively, the base relation encodes axioms satisfied by combinations of primitive effects. It is the only part of the $\equiv_F$ relation that is specific to $F$: we sometimes say that the base relation *generates* $\equiv_F$;

- then, $\equiv_F$ is closed under *reflexivity*, *symmetry*, and *transitivity*;

- next, in order to take into account the CPO structure of interaction trees, $\equiv_F$ is a congruence w.r.t. *lub*. Specifically, for any two directed sets $S, S'$ such that for each $s \in S$ there exists $s' \in S'$ with $s' \equiv_F s$, and conversely, for each $s' \in S'$ there exists $s \in S$ with $s \equiv_F s'$, we have *lub* $S \equiv_F \textit{lub } S'$;

- finally, in order to take into account the CPO-monad structure of interaction trees, $\equiv_F$ is a congruence w.r.t. *bind*. Specifically, for all $X, Y \in Set m, m' \in itree F X$ and $f, f' : X \to itree F Y$ if $m \equiv_F m'$ and for all $x \in X, f x \equiv_F f' x$ then *bind* $m f \equiv_F \textit{bind } m' f'$.

**Remark 21.** We emphasize that each $\equiv_F$, being the smallest relation satisfying the above constraints, is an *inductively* defined relation. An inductively-defined relation has the advantage of enabling proofs by induction; for example, the proof of correctness of $\equiv$ critically depends on induction being available$^7$. A potential drawback of an inductive relation for interaction trees modeling programs is that each pair of programs must be proven equivalent in *finitely* many steps; this may appear to rule out equivalence proofs for *infinitely-running*, i.e., non-terminating programs, be they recursive or corecursive. This pitfall is avoided by $\equiv_F$ being a congruence for *lub*: non-terminating programs are the *lubs* of their finite approximations; the congruence to *lub* thus reduces the equivalence of non-terminating programs to equivalences of their respective finite approximations which, being terminating, are adequately handled by induction.

**Example 22.** The congruence relation for the effect signature $F = State_S$ (Example 17) is generated by the base relation {((put x; put y), put x), ((put x; get), (put x; ret x)), ((do x ← get; put x), (ret *)), (do x ← get; do y ← get; f x y), (do x ← get; f x x))}, implicitly universally quantified over the free variables. Here, and *ret* and *bind* (under the *do* notation) are those of the interaction-tree state CPO monad *itree State*$_S X$, with *$*$ being the unique value in the unit set **1**.

**Example 23.** For the effect signature $F = Prob$ (cf. Example 16) the base relation includes pairs such as ((Flip $p$; $m$), $m$), for all $X \in Set$ and $m \in itree Prob X$; (Flip 0, *ret* false); (Flip 1, *ret* true); and (Flip (1 - $p$), (do $b \leftarrow$ Flip $p$; *ret* $
eg b$)), for all $p \in [0, 1]$; and several others, not shown here from lack of space. The first set of pairs say that if the Boolean returned by **Flip** is not used, it can be returned; the second and third say that the “corner cases” **Flip** 0, resp. **Flip** 1 amount to returning **false**, resp. **true**; and the fourth set of pairs state that performing **Flip** (1 - $p$) amounts to performing **Flip** $p$ and return the negation of its result.

<footnote>$^7$ Specifically, we have designed a customized induction principle for $\equiv$ and have proved it sound in Rocq.</footnote>
# 5 Coproduct

Monads are commonly used to model computational effects. To combine effects, we need principled ways to combine monads. While ad-hoc approaches like distributive laws [7] or monad transformers [19] exist, a more canonical solution is to use the notion of coproduct [17].

We start with general definitions of CPO-monad morphism and coproduct. We then instantiate the definitions to CPO-monads of interaction trees. Finally, we show how the base relations of two interaction trees can also be combined, resulting in a global congruence specific to their coproduct.

## 5.1 CPO-monad Morphism

A CPO-monad morphism is a map that translates computations from one CPO-monad to another while preserving their CPO-monadic structure. For this translation to be semantically sound, the morphism must satisfy four key properties:

First, it is strict, i.e., it maps an undefined computation in the source monad to an undefined computation in the target monad. Second, it is continuous, i.e., it respects limits, ensuring that the output for an infinite computation is defined by the limit of the outputs for its finite approximations [11].

Third, the morphism commutes with `ret`. It ensures that the computations without any observable effect are translated identically. Fourth, the morphism commutes with `bind`. This property ensures that the sequential structure of computation and the dependency of effects is preserved. Translating a composite computation is equivalent to first translating its constituent parts and then forming their composition within the target monad.

**Definition 24.** Given two CPO-monads $(M_1, ret^{M_1}, bind^{M_1})$ and $(M_2, ret^{M_2}, bind^{M_2})$, a CPO-monad morphism between them consists of a family of strict continuous functions $f_X : M_1 X \to M_2 X$ (for each set $X$) preserving `ret` and `bind`:

$$ \underline{\forall X \forall x \in X, f_X(ret^{M_1} x) = ret^{M_2} x} $$

$$ \underline{\forall X Y (m : M_1 X) (f : X \to M_1 Y), f_Y(\mathrm{do } x \leftarrow m; f x) = \mathrm{do } x \leftarrow f_X m; f_Y(f x)} $$

## 5.2 CPO-monad Coproduct

**Definition 25.** Given two CPO-monads $M_1$ and $M_2$, their coproduct is a CPO-monad $M_1 + M_2$ equipped with CPO-monad morphisms $\iota_1 : M_1 \to M_1 + M_2$ and $\iota_2 : M_2 \to M_1 + M_2$ such that for any CPO-monad $M$ and CPO-monad morphisms $f : M_1 \to M$, $g : M_2 \to M$, there exists a unique $[f, g] : M_1 + M_2 \to M$ such that $[f, g] \circ \iota_1 = f$ and $[f, g] \circ \iota_2 = g$ (where $\circ$ denotes function composition)

## 5.3 Coproduct of interaction-tree CPO-Monads

Coproducts do not exist for all monads, and their construction can be complex when they do exist. However, the coproduct of interaction-tree CPO-monads does exist and is constructed analogously to the coproduct of free monads [24]. Intuitively, just as a coproduct in set theory allows elements from either of two sets, the coproduct of monads allows effects from either of two effect signatures to be combined into a single monad that understands both.

Let $F$ and $G$ be effect signatures. The coproduct of the interaction-tree monads `itree F` and `itree G` is given by `itree (F + G)` where $F + G$ denotes the pointwise sum $\lambda X. F X + G X$. Conceptually, this means we create a new effect signature that contains all the operations from both $F$ and $G$, tagged to indicate their origin.
This coproduct is equipped with the following injections defined by using our *fold* function on interaction trees (cf. Section 4.2.2):

■ The injection $\iota_F : \mathit{itree} F \to \mathit{itree} (F + G)$ is defined by:

$$ \text{fold ret} (\lambda fy. \lambda k. \text{impure} (\text{inl fy}) k) m $$

■ The injection $\iota_G : \mathit{itree} G \to \mathit{itree} (F + G)$ is defined by:

$$ \text{fold ret} (\lambda fy. \lambda k. \text{impure} (\text{inr fy}) k) m $$

The intuition behind these injections is straightforward: they take computations from either monad and systematically tag all their effect operations with inl or inr to indicate whether they came from F or G. This tagging preserves the structure of the original computation while making it compatible with the combined effect signature.

Given monad morphisms $f : \mathit{itree} F \to M$ and $g : \mathit{itree} G \to M$ into some common monad $M$, the unique monad morphism $[f, g] : \mathit{itree} (\lambda X. F X + G X) \to M$ is defined by $\text{fold ret h}$ where:

$$ h (\text{inl fx}) = \lambda k. \text{do } x \leftarrow f (\text{trigger fx}); k x $$

$$ h (\text{inr gx}) = \lambda k. \text{do } x \leftarrow g (\text{trigger gx}); k x $$

The key idea here is that $[f, g]$ pattern-matches on the tagged effects: if it encounters an F-effect (tagged with inl), it handles it using *trigger* (cf. Definition 18) and $f$; if it encounters a G-effect (tagged with inr), it handles it using *trigger* and $g$. This ensures that both types of effects are properly interpreted in the target monad $M$.

One can then verify that the injections $\iota_F$ and $\iota_G$ are indeed monad morphisms (cf. Definition 24) and that this construction satisfies the universal property of a coproduct (cf. Definition 25). The universal property guarantees that this is the most general way to combine $\mathit{itree} F$ and $\mathit{itree} G$ while preserving their individual structures.

**► Example 26 (Probability-state effect signature).** We have seen the individual *Prob* and *State* effect signatures in Examples 17 and 16 above. The coproduct of the corresponding interaction-tree CPO-monads yields an interaction tree with the combined signature *ProbState* effect signature. This signature inherits the state operations *get* and *put* from the *State* effect signature, alongside the probabilistic operation *flip* $p$ from the *Prob* effect signature.

## 5.4 Congruence for Equational Reasoning

Given two base relations $R_F$ and $R_G$, we define a base relation $R_{F+G}$ as the union of $R_F$ and $R_G$, together with an additional relation encoding the interactions between the corresponding effects. Among the possible interactions, we here restrict ourselves to commutativity, which is in some sense the unit element of interactions.

Specifically, for any effect $fx$ in $F$ and $gy$ in $G$, triggering $fx$ followed by $gy$ is related to triggering $gy$ followed by $fx$. Formally, we define $R_{F+G}$ by:

$$ R_F \cup R_G \cup \left\{ \left( \begin{array}{l} \text{do } x \leftarrow \iota_F(\text{trigger fx}); \\ y \leftarrow \iota_G(\text{trigger gy}); \\ \text{ret } (x, y) \end{array} , \begin{array}{l} \text{do } y \leftarrow \iota_G(\text{trigger gy}); \\ x \leftarrow \iota_F(\text{trigger fx}); \\ \text{ret } (x, y) \end{array} \right| \begin{array}{l} X, Y \in \text{Set} \\ fx \in F X \\ gy \in G Y \end{array} \right\} $$

Following Section 4.3, we take the congruence closure of $R_{F+G}$ to obtain $\equiv_{F+G}$. This guarantees that the equational theories of $F$ and $G$ are embedded into the coproduct, while the commutativity law establishes the mutual independence of the two effect signatures.
590

591

592

593

► **Example 27** (Probability-state congruence relation). The congruence $\equiv_{ProbStates}$ simultaneously enforces the individual laws for state and probability, but also the commutativity law that makes the operations of each signature independent. For instance, a sequence that first flips a coin and then updates the state is equivalent with a sequence that first updates the state and then flips a coin.

594

595

596

Of course, one still has to prove that $\equiv_{F+G}$ is correct. For the case of commutativity, which here interests us, a key step in proving the correctness of $\equiv_{F+G}$ is to show that denotations are preserved when the order of individual effects from *F* and from *G* is changed.

597

598

599

600

601

602

603

604

► **Example 28** (Probability-state correctness). The correctness of $\equiv_{ProbStates}$ rests on two separate foundations. First, the correctness of the individual congruences $\equiv_{Prob}$ and $\equiv_{States}$ must be established independently, verifying that their respective equations are sound with respect to the denotational semantics in the CPO-monad combining state and probability defined at the end of Section 3. Then, proving the correctness of $\equiv_{ProbStates}$ reduces to showing that the denotational semantics is preserved when commuting a **Flip** (*p*) effect with a **get** or **put** effect. This holds because the probabilistic choices are independent of the state transformations: the coin flip does not depend on the current state, and updating the state does not affect the bias of the coin.

605

# 6 Applications

606

607

608

609

The principal advantage of our interaction-tree monad is that it allows one to reason equationally about the program’s syntactic specification independently of the effectful semantics given later by an interpreter. This separation is absent in standard monads, where the program’s logic and its execution are fused.

610

611

612

613

We illustrate this on two examples. The first one is the equivalence of two possibly non-terminating programs using the *States* effect signature. The second one establishes the correctness of a possibly non-terminating program using the combined *States* and *Prob* effect signature, by proving it equivalent to a more abstract reference implementation.

614

## 6.1 Syracuse

615

616

617

618

619

The Syracuse problem is a well-known open mathematical conjecture about the finiteness of a sequence of natural numbers. We do not, of course, solve the conjecture, but merely show that two programs enumerating the elements in the sequence in two different ways are equivalent for the congruence $\equiv_{States}$. By the correctness of this relation, the denotations of the two programs are equal; in particular, the denotations both either terminate with the same output, or they both diverge.

620

621

622

623

The two programs are respectively shown in Figures 3 and 4. Both start with an initial natural-number value *n*, and both have a state containing a natural number: the current value in the Syracuse sequence. Moreover, both programs use while-loops, introduced in our setting in Example 3: *syracuse_single* in Figure 3 uses one loop, and *syracuse_double* in Figure 4 uses two nested loops.

624

625

626

627

The program *syracuse_double* can be seen as an optimized version of *syracuse_single*: while the current value in the state is even, it is repeatedly divided by 2 until it is not even anymore (or forever, if the current value is 0). In our Rocq implementation we use a binary representation of natural numbers, where repeated division by 2 amounts to removing all zeroes at the end of the number.

628

629

630

631

632

Both programs use the basic primitives **put** to write in the state and **get** to read from it. Being monadic programs, the “local variables” occurring in “assignments”, such as *x* in do *x* ← *do*..., have a rather narrow “scope”, which is why reading/writing the state occurs more often than it would in an actual imperative language with broader scope for local variables. Everything happens as if the scope of local variables were limited to the sub-programs for the loop’s condition and body, respectively.
```pascal
syracuse_single(n : N) :=
  put n;
while (do x ← get; ret (x ≠ 1))
  {
    do x ← get;
    if even x then
      put (x div 2)
    else
      put (3 x + 1)
  }
get.
```

<caption>Figure 3 Single-loop *Syracuse* function.</caption>

```pascal
syracuse_double(n : N) :=
  put n;
while (do x ← get; ret (x ≠ 1))
  {
    do x ← get;
    if even x then
      while (do y ← get; ret (even y))
        {
          do x ← get;
          put (x div 2)
        }
    else
      put (3 x + 1)
  }
get.
```

<caption>Figure 4 Double-loop *Syracuse* function.</caption>

Note also that both programs end with `get`, which, given the conditions of the while-loops, implies that they return 1 if they terminate. The programs definitely do not terminate when starting with initial value `n = 0`: for `syracuse_single` the (unique) while-loop does not terminate because its condition (`state value = 1`) is always false; for `syracuse_double` it is actually the inner loop that does not terminate. Of course, the termination status for all other inputs is, in general, unknown, and, by proving their equivalence, we prove that they either both terminate (with value 1) or do not terminate. The relation between the two programs is formally stated as follows.

**Theorem 29.** For all $n \in \mathbb{N}$, `syracuse_single` $n \equiv_{\text{StateN}}$ `syracuse_double` $n$.

We now give an outline of the proof. For $k \in \mathbb{N}$, let $nb\_zeroes : \mathbb{N} \to \mathbb{N}$ be defined as follows: $nb\_zeroes 0 = 0$, and, for $k > 0$, $nb\_zeroes k$ is the highest power of 2 that divides $k$. Next, let `while_fuel` be the function recursively defined on $i \in \mathbb{N}$ by

```pascal
while_fuel 0 cond body = ⊥
while_fuel (i + i) cond body = do b ← cond;
  body; while_fuel i cond body if b = true
  ret * if b = false
```

That is, `while_fuel i cond body` is the $i$-th iteration of the functional for the while-loop with given condition and body. By Kleene's theorem, `while cond body = lub {while_fuel i cond body | i \in \mathbb{N}}`.

We now focus on the inner while-loop of `syracuse_double`, and prove by induction on $x \ge 1$ (the value of the state before the loop) that the `lub` is reached in $nb\_zeroes x$ iterations. In the remaining case $x = 0$, the `lub` equals $\perp$, i.e., the inner loop diverges; otherwise the loop terminates in $nb\_zeroes x$ iterations, and upon termination the state's updated value is $x/(2^{nb\_zeroes x})$.

Next, consider the two other while-loops in the programs and their representation as `lubs` of while-loops with fuel given by Kleene's theorem. We distinguish the cases $n = 0$ and $n > 0$.

- if $n = 0$: we are in the case where the inner loop of `syracuse_double` does not terminate; its value $\perp$ propagates to the outer loop and to the whole program; hence `syracuse_double 0 = \perp`. The same kind of reasoning establishes `syracuse_simple 0 = \perp`, and `syracuse_single 0 \equiv_{\text{StateN}} syracuse_double 0` results from $\equiv_{\text{StateN}}$ being reflexive, which proves our theorem for $n = 0$.

- If $n \ne 0$, we note that, thanks to additional iterations of the inner loop, every iteration of the outer loop of `syracuse_double` corresponds to one or more iterations of the loop of `syracuse_simple`,
where "corresponds" means "result in the same value of the state". More precisely, we prove by induction on $k$ that the $k$-th iteration of the outer loop of `syracuse_double` corresponds to the iteration number `iter n k` of the loop of `syracuse_simple`, where `iter n k` is the function recursively defined on $k$ shown in Figure 5. Thanks to the congruence of $\equiv_{State_N}$ w.r.t. `bind` and to properties of `lub` (specifically, that `bind` and `lub` commute, due to the continuity of `bind` in both arguments), the statement of the theorem in the current case $n \neq 0$ can be rewritten as follows:

$$ lub \{syracuse_single_fuel k n \mid k \in \mathbb{N}\} \equiv_{State_N} lub \{syracuse_double_fuel (iter n k) n \mid k \in \mathbb{N}\} $$

where `syracuse_single_fuel k n` is like `syracuse_single n`, except that its while loop is replaced by a while-fuel with fuel $k$; and `syracuse_double_fuel (iter n k) n` is like `syracuse_double n`, except that its outer while loop is replaced by a while-fuel with fuel `iter n k`. Next, since $\equiv_{State_N}$ is a congruence for `lub`, the statement of the theorem amounts to: for all $k, n \in \mathbb{N}$ with $n \neq 0$, `syracuse_single_fuel k n \equiv_{State_N} syracuse_double_fuel (iter n k) n$, which is proved by induction on $k$. We note that equational reasoning with respect to the base relation occurs in the goal of the inductive step, simplifying and preparing it for the application of the induction hypothesis.

iter n k :=
    case k of
        0 ⇒ 0
        1 + j ⇒ if n = 1 then k
            else if even n then iter (n/2^nb_zeroes n) j + nb_zeroes n
            else iter (1 + 3n) j
    end

<caption>Figure 5 Correspondence between iterations of outer loops, when $n \neq 0$.</caption>

► Remark 30. The creative choices in our congruence proof regard iterations of the loops, "counted" using the functions `nb_zeroes` and `iter`. These are specific to this particular problem. The rest of the proof is specific to our approach. It uses properties of `lub`, in particular, that `bind` and `lub` commute, thanks to the continuity of `bind` in both arguments and the congruence properties for `bind` and `lub`.

## 6.2 Flip While True

This is a simple example illustrating the combined effect signature `ProbState_S` with $S = \mathbb{N}$ and the corresponding congruence $\equiv_{ProbState_N}$. The `flipwhile_true` function in Figure 6 initializes its state (a natural-number counter) to 0 and then, using a while loop, gets a random Boolean `Flip(p)`, where the real-number $p \in [0, 1]$ is a parameter of the function. If the Boolean is `true`, the counter is increased, and the process is repeated until the Boolean becomes `false`. The function ends by returning the value of the state using `get`.

Hence, the function `flipwhile_true` achieves a geometric probability distribution over natural numbers: each $n \in \mathbb{N}$ is returned by the function with probability $p^n (1-p)$.

Formally, `flipwhile_true p \in itree ProbState_N \mathbb{N}`, where the second $\mathbb{N}$ is the type of the returned value. In order to formally prove that `flipwhile_true` correctly implements the geometric distribution, we prove that it is equivalent according to $\equiv_{ProbState_N}$ to another tree in `itree ProbState_N \mathbb{N}`, which is in some sense a more abstract specification of the geometric distribution: the recursive function `geom` in Figure 7. The `geom` function gets a random Boolean using `Flip(p)` and recursively calls itself with its parameter $n$ increased by one, or returns $n$, depending on the Boolean it got. When the function
flipwhile_true(p : [0, 1]) :=
    put 0;
while (do x ← Flip (p); ret x)
    {{
        do x ← get;
        put(x + 1);
    }}
get.

geom(p : [0, 1])(n : N) :=
    do x ← Flip (p)
    if x then
        do dummy ← get;
        put (dummy + 1);
        geom p (n + 1)
    else
        ret n.

■ **Figure 6** Geometric distribution: implementation... ■ **Figure 7** ...and specification.

calls itself it also increments a dummy counter in its state by 1; the counter does not influence geom but helps us to prove the theorem:

683

684

► **Theorem 31.** For all reals $p \in [0, 1]$, flipwhile_true $p \equiv_{ProbState_{\mathbb{N}}} \text{geom} p 0$.

685

► **Remark 32.** We note that the implementation and specification are by no means equal as interaction trees. The uninterpreted effects on the state are quite different: a simple examination shows that the state plays no role in the specification, while in the implementation the state is essential: it is the function's result, returned by **get**.

686

687

688

689

The proof of Theorem 31 is similar to that of the previous theorem stating congruence, Theorem 29. The *geom* function is replaced, using Kleene's theorem, as the *lub* of the approximations *geom_fuel f* of *geom* with finite fuel *f* ∈ N. The same process happens with *flipwhile_true*. We then prove that for all *f* ∈ N, *flipwhile_true_fuel f* *p* ≡<sub>*ProbState<sub>\N</sub></sub> *geom_fuel* (*f* + 1) *p* 0, where the offset 1 is due to the fact that *geom_fuel* 0 *p* 0 = ⊥, but *flipwhile_true_fuel* 0 *p* ≠ ⊥ because of the initial **put** 0.

690

691

692

693

694

The proof goes by induction on *f*, and equational reasoning is used in the induction step to prepare the goal for applying the induction hypothesis. The equational reasoning uses the combined equations of $R_{Prob+States}$ (cf. Section 5.4): those in $R_{States}$, those of $R_{Prob}$, and the additional equations describing the commutativity of basic effects of *States* and *Prob* in their coproduct.

695

696

697

698

## 7 Conclusions and Future Work

699

In this paper we have presented a novel domain-theoretic formalization of interaction trees in Rocq that provides a principled foundation for reasoning about effectful, potentially non-terminating computations. Our approach offers several significant advantages over existing frameworks. First, by grounding interaction trees in domain theory, we eliminate the need for silent transitions and weak bisimulation that complicate reasoning in standard interaction tree frameworks [27]. Second, our framework naturally supports modular effect composition through coproducts of interaction-tree monads. Each effect is specified independently by its equational theory, and when combined via coproduct, these equations integrate seamlessly without requiring distributive laws [7] or ad-hoc monad transformers [19]. Each effect in our framework is specified independently by its equational theory, and when combined via coproduct, these equations integrate seamlessly. This modularity ensures extensibility: new effects can be added without reengineering existing proofs. Third, our equational reasoning style substantially simplifies verification compared to operational semantics approaches like FreeSpec [16, 15] which struggles with nondeterministic and probabilistic effects, whereas our framework handles these naturally. And unlike Monae's type-class-based abstraction [4], our interaction-tree monads provide a uniform mathematical representation of effectful components. Finally, we have demonstrated the practical utility of our approach through non-trivial examples, including the verification of a stateful probabilistic program and the equivalence proof for two

700

701

702

703

704

705

706

707

708

709

710

711

712

713

714

715

716
implementations of the Syracuse sequence. These case studies illustrate how our framework supports reasoning about effect interactions and potentially non-terminating computations.

Several promising directions emerge for future research. While we have focused on foundational effects like state and probability, the framework could be extended to support other important effects such as concurrency, input/output, and continuations. Developing the corresponding equational theories and verifying their integration through coproducts would demonstrate the full generality of the approach. The equational nature of our framework suggests opportunities for enhanced automation. Specialized tactics for effect-specific reasoning and coproduct manipulation could be developed, building on Rocq's existing rewriting capabilities to provide more seamless verification experiences. Combining the domain-theoretic interaction trees with program logics (such as Hoare logic or separation logic) could enable even more powerful verification strategies. This integration would support mixed equational and logical reasoning about effectful programs.

Our work establishes a solid foundation for modular, equational reasoning about effectful computations in proof assistants, bridging the gap between categorical abstractions and practical verification needs. This approach scales to increasingly complex effect interactions while maintaining the rigor and automation essential for verified software development.

References

1 Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. *Theor. Comput. Sci.*, 342(1):3–27, 2005. doi:10.1016/j.tcs.2005.06.002.

2 Reynald Affeldt, Jacques Garrigue, David Nowak, and Takafumi Saikawa. A trustful monad for axiomatic reasoning with probability and nondeterminism. *J. Funct. Program.*, 31:e17, 2021. doi:10.1017/S0956796821000137.

3 Reynald Affeldt and David Nowak. Extending equational monadic reasoning with monad transformers. In Ugo de'Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, *26th International Conference on Types for Proofs and Programs, TYPES 2020, March 2-5, 2020, University of Turin, Italy*, volume 188 of LIPIcs, pages 2:1–2:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.TYPES.2020.2, doi:10.4230/LIPICS.TYPES.2020.2.

4 Reynald Affeldt, David Nowak, and Takafumi Saikawa. A hierarchy of monadic effects for program verification using equational reasoning. In Graham Hutton, editor, *Mathematics of Program Construction - 13th International Conference, MPC 2019, Porto, Portugal, October 7-9, 2019, Proceedings*, volume 11825 of Lecture Notes in Computer Science, pages 226–254. Springer, 2019. doi:10.1007/978-3-030-33636-3_9.

5 Roberto M. Amadio and Pierre-Louis Curien. *Domains and lambda-calculus*, volume 46 of Cambridge Tracts in theoretical computer science. Cambridge University Press, 1998.

6 Philippe Audebaud and Christine Paulin-Mohring. Proofs of randomized algorithms in coq. *Sci. Comput. Program.*, 74(8):568–589, 2009. URL: https://doi.org/10.1016/j.scico.2007.09.002, doi: 10.1016/J.SCICO.2007.09.002.

7 Jon Beck. Distributive laws. In B. Eckmann, editor, *Seminar on Triples and Categorical Homology Theory*, pages 119–140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg.

8 Nicolas Chappe, Paul He, Ludovic Henrio, Eleftherios Ioannidis, Yannick Zakowski, and Steve Zdancewic. Choice trees: Representing and reasoning about nondeterministic, recursive, and impure programs in rocq. *J. Funct. Program.*, 35, 2025. URL: https://doi.org/10.1017/s0956796825100105, doi:10.1017/S0956796825100105.

9 Jeremy Gibbons and Ralf Hinze. Just do it: simple monadic equational reasoning. In Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy, editors, *Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011*, pages 2–14. ACM, 2011. doi:10.1145/2034773.2034777.

10 Patricia Johann, Alex Simpson, and Janis Voigtländer. A generic operational metatheory for algebraic effects. In *Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS*
2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 209-218. IEEE Computer Society, 2010.
doi:10.1109/LICS.2010.29.

11 Gilles Kahn. The semantics of a simple language for parallel programming. In Jack L. Rosenfeld, editor, *Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974*, pages 471-475. North-Holland, 1974.

12 Oleg Kiselyov and Hiromi Ishii. Freer monads, more extensible effects. In Ben Lippmeier, editor, *Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015, Vancouver, BC, Canada, September 3-4, 2015*, pages 94-105. ACM, 2015. doi:10.1145/2804302.2804319.

13 Nicolas Koh, Yao Li, Yishuai Li, Li-yao Xia, Lennart Beringer, Wolf Honoré, William Mansky, Benjamin C. Pierce, and Steve Zdancewic. From C to interaction trees: specifying, verifying, and testing a networked server. In Assia Mahboubi and Magnus O. Myreen, editors, *Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019*, pages 234-248. ACM, 2019. doi:10.1145/3293880.3294106.

14 Ugo Dal Lago, Francesco Gavazzo, and Paul Blain Levy. Effectful applicative bisimilarity: Monads, relators, and howe's method. In *32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017*, pages 1-12. IEEE Computer Society, 2017. doi:10.1109/LICS.2017.8005117.

15 Thomas Letan and Yann Régis-Gianas. Freespec: specifying, verifying, and executing impure computations in coq. In Jasmin Blanchette and Catalin Hritcu, editors, *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020*, pages 32-46. ACM, 2020. doi:10.1145/3372885.3373812.

16 Thomas Letan, Yann Régis-Gianas, Pierre Chiflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in coq. In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik P. de Vink, editors, *Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 15-17, 2018, Proceedings*, volume 10951 of Lecture Notes in Computer Science, pages 338-354. Springer, 2018. doi:10.1007/978-3-319-95582-7\_20.

17 Christoph Lüth and Neil Ghani. Composing monads using coproducts. In Mitchell Wand and Simon L. Peyton Jones, editors, *Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002*, pages 133-144. ACM, 2002. doi:10.1145/581478.581492.

18 Eugenio Moggi. Computational lambda-calculus and monads. In *Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), Pacific Grove, California, USA, June 5-8, 1989*, pages 14-23. IEEE Computer Society, 1989. doi:10.1109/LICS.1989.39155.

19 Eugenio Moggi. A modular approach to denotational semantics. In David H. Pitt, Pierre-Louis Curien, Samson Abramsky, Andrew M. Pitts, Axel Poigné, and David E. Rydeheard, editors, *Category Theory and Computer Science*, pages 138-139, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg.

20 Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55-92, 1991. doi:10.1016/0890-5401(91)90052-4.

21 Lucas Silver, Eddy Westbrook, Matthew Yacavone, and Ryan Scott. Interaction tree specifications: A framework for specifying recursive, effectful computations that supports auto-active verification. In Karim Ali and Guido Salvaneschi, editors, *37th European Conference on Object-Oriented Programming, ECOOP 2023, July 17-21, 2023, Seattle, Washington, United States*, volume 263 of LIPIcs, pages 30:1-30:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2023.30, doi:10.4230/LIPICS.ECOOP.2023.30.

22 Alex Simpson and Niels F. W. Voorneveld. Behavioural equivalence via modalities for algebraic effects. In Amal Ahmed, editor, *Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings*, volume 10801 of Lecture Notes in Computer Science, pages 300-326. Springer, 2018. doi:10.1007/978-3-319-89884-1\_11.

23 Viggo Stoltenberg-Hansen, Ingrid Lindström, and Edward R. Griffin. *Mathematical theory of domains*, volume 22 of *Cambridge tracts in theoretical computer science*. Cambridge University Press, 1994.
817

24 Wouter Swierstra. Data types à la carte. *J. Funct. Program.*, 18(4):423–436, 2008. doi:10.1017/S0956796808006758.

818

819

25 Philip Wadler. Monads for functional programming. In Manfred Broy, editor, *Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28 - August 9, 1992*, volume 118 of NATO ASI Series, pages 233–264. Springer, 1992. doi:10.1007/978-3-662-02880-3\_8.

820

821

822

823

26 G. Winskel. *The Formal Semantics of Programming Languages, an introduction*. MIT Press, 1993.

824

27 Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees: representing recursive and impure programs in Coq. *Proc. ACM Program. Lang.*, 4(POPL):51:1–51:32, 2020. doi:10.1145/3371119.

825

826

827

8 Appendix.

828

We give an overview of the definition of interaction trees from the companion Rocq development.

829

The definition is based on an encoding of coinductive types can be constructed from inductive types endowed with definition orders, using the completion and closure operations presented in Section 2. The motivation is that, in Rocq, inductive types are well-supported; by contrast, everything coinductive is quite limited. The resulting types are kin to (unary) *containers* [1], a rich class of types that include all *strictly positive* types built with constants, sums, products, exponentiation by sets, and fixpoints. There are, however, differences: the main one is that our coinductive types are inhabited not only by fully defined (maximal) terms, but also by their partially-defined approximations.

830

831

832

833

834

835

836

We recap below the main relevant definitions from our Rocq development.

837

We use a set-theoretic presentation. The *carrier* of a function $f : X \to Y$, where $Y$ contains a value $\perp$, is the pre-image by $f$ of $Y \setminus \{\perp\}$ and is denoted by $\llbracket f \rrbracket$.

838

839

► **Definition 33 (Finite Labelled Partial Container (FLPC))**. *Given a set *A* of shapes and two functions *L* and *B* that for each *a* ∈ *A* produce a set (*L* a) of labels and respectively a set (*B* a) of positions, the finite labelled partial container (*FLPC*) *C*° parameterized by *A*, *L*, and *B*, is the set inductively defined by the rules: *⊥* ∈ *C*°, and, for all *a* ∈ *A*, *l* ∈ *L* a, and *f* : (*B* a) → *C*° such that* $\llbracket f \rrbracket$ *is finite, node*° *a* *l* *f* ∈ *C*°.*

840

841

842

843

844

Intuitively, FLPCs are either leaves ($\perp$), or labelled trees of finite depth and of possibly infinite breadth, with only finitely many subtrees not being leaves.

845

846

► **Definition 34 (Definition Order).** *The order $\leq^o$ on $C^o$ is inductively defined by: $\perp \leq^o c^o$ for all $c^o \in C^o$, and $node^o a l f \leq^o node^o a l f'$ whenever for all $b \in (B a)$, $f b \leq^o f' b$.*

847

848

The definition order organizes an FLPC as a PPO ($C^o, \leq^o, \perp$).

849

**Notation.** Assume a given FLPC $C^\circ$ parameterized by shapes $A$, labels $L$, and positions $B$, and organized as a PPO $(C^\circ, \leq^\circ, \perp)$. For all $a \in A$, we denote by $F_a^\circ$ the set $\{f^\circ : (B a) \to C^\circ \mid \llbracket f^\circ \rrbracket \text{ is finite}\}$. The relation $\sqsubseteq^\circ$ on $F_a^\circ$ denotes the pointwise order: $f^\circ \sqsubseteq^\circ f'^\circ$ iff for all $b \in (B a)$, $f b \leq^\circ f' b$. Let also $\perp_a$ denote the constant function $\lambda_\perp : (B a) \to \perp \in F_a^\circ$.

850

851

852

853

With the above notations, for all $a \in A$, $(F_a^\circ, \sqsubseteq_a, \perp_a)$ is a PPO. Moreover, for all $a \in A$ and $l \in L_a$, the functions $node^o a l : F_a^\circ \to C^\circ$ are poset morphisms, i.e., they are monotonic: for all $f^\circ, f'^\circ \in F_a^\circ$, $f^\circ \sqsubseteq_a f'^\circ$ implies $node^o a l f^\circ \leq_a node^o a l f'^\circ$.

854

855

856

The completion operation, seen in Section 2.3, turns the PPO ($C^\circ, \leq^\circ, \perp$) into an ACPO ($C, \leq, \perp$), such that ($C^\circ, \leq^\circ$) is the poset of compacts of ($C, \leq$).

857

We call *Labelled Partial Containers (LPCs)* the completions of FLPCs.

858
**Notation.** If $C^\circ$ is an FLPC with shapes $A$, labels $L$, and positions $B$, and the LPC $(C, \leq, \perp)$ is the completion of $(C^\circ, \leq^\circ, \perp)$, then for all $a \in A$, we let $F_a$ denote the set $(B a) \to C$. A relation $\sqsubseteq_a$ on $F_a$ is defined by $f \sqsubseteq_a f'$ iff for all $b \in (B a)$, $f b \leq f' b$.

Then, by the closure of ACPOs under exponentiation, $(F_a, \sqsubseteq_a, \perp_a)$ is an ACPO whose PPO of compacts is $(F_a^\circ, \sqsubseteq_a^\circ, \perp_a)$, which amounts to saying that $(F_a, \sqsubseteq_a, \perp_a)$ is a completion of $(F_a^\circ, \sqsubseteq_a^\circ, \perp_a)$. Hence, from each monotonic function $node^\circ a l : F_a^\circ \to C^\circ$ one obtains, by function-completion, a unique continuous function $node a l : F_a \to C$ satisfying $node a l f_a^\circ = node^\circ a l f_a^\circ$ for all $f_a^\circ \in F_a^\circ$. Moreover, the functions $node^\circ a l$ behave as constructors for $C$, which, in turn, behaves like a coinductive type:

- for all $c \in C$, $c = \perp$ or (exclusively) there exist unique $a \in A$, $l \in L$ and $f \in F_a$ such that $c = node a l f$;

- one can coinductively define an order $\leq \subseteq C \times C$, whose *unfolding equation* states that $c \leq c'$ iff $c = \perp$ or there exist $a \in A$, $l \in L$ and $f, f' \in F_a$ such that $c = node a l f$, $c' = node a l f'$ and, for all $b \in (B a)$, $(f b) \leq (f' b)$;

- the definition order gives rise to a *bisimulation relation* $\approx \subseteq C \times C$, defined by $t \approx t'$ iff $t \leq t'$ and $t' \leq t$, whose *unfolding equation* states that $c \approx c'$ iff $c = c' = \perp$ or there exist $a \in A$, $l \in L$ and $f, f' \in F_a$ such that $c = node a l f$, $c' = node a l f'$ and, for all $b \in (B a)$, $(f b) \approx (f' b)$;

- the bisimulation relation satisfies the following *coinduction principle*: in order to prove $c \approx c'$, find $R \subseteq C \times C$ with $(c, c') \in R$ and prove that for all $(u, v) \in R$, $u = v = \perp$ or $u = node a l f$, $v = node a l f'$ for some $a \in A$, $l \in L$ and $f, f' \in F_a$ such that for all $b \in (B a)$, $((f b), (f' b)) \in R$;

- bisimulation coincides with equality: to prove $c = c'$ one can equivalently prove $c \approx c'$.

We now define interaction trees as an instance of FLPCs. We start with a definition of *finite* interaction trees as Labeled Finite Partial Containers (LFPCs) and then use completion, cf. Section 2.3.

**► Definition 35 (Finite Interaction Tree).** A finite interaction tree $itree^\circ F X$ parameterized by a partial function $F : \text{Set} \to \text{Set}$ (the effect signature) and a set $X$ is inductively by the rules

- $\perp \in itree^\circ F X$;

- for all $x \in X$, $\text{pure}^\circ x \in itree^\circ F X$;

- for all $Y \in \text{Set}$, $fy \in F Y$, and $k : Y \to itree^\circ F X$ such that $\llbracket k \rrbracket$ is finite, $\text{impure}^\circ fy k \in itree^\circ F X$.

Next, we identify the instance of FLPC (cf. Def. 33) that encodes finite interaction trees:

**► Definition 36.** For $F : \text{Set} \to \text{Set}$ and $X \in \text{Set}$, we define an FLPC $\mathcal{L}^\circ F X$ with the following parameters:

- the of shapes set $A$ is the disjoint union $1 + \text{Set}$;

- $B : A \to \text{Set}$ is defined by $B (\text{inl} \ *) = \emptyset$ and $B (\text{inr} Y) = Y$ for all $Y \in \text{Set}$;

- $L : A \to \text{Set}$ is defined by $L (\text{inl} \ *) = X$ and $L (\text{inr} Y) = F Y$ for all $Y \in \text{Set}$.

The constructors of $itree^\circ F X$ are encoded as using the constructors of $\mathcal{L}^\circ F X$ as follows:

- $\perp \in itree^\circ F X$ is encoded by $\perp \in \mathcal{L}^\circ F X$;

- for all $x \in X$, $\text{pure}^\circ x$ is encoded by $node^\circ (\text{inl} \ *) x$ ($\lambda_\_ : \emptyset \to X$), where $\lambda_\_ : \emptyset \to X$ is the unique element of $\emptyset \to X$;

- for all $Y \in \text{Set}$, $fy \in F Y$ and $k \in Y \to itree^\circ F X$ with $\llbracket k \rrbracket$ finite, $\text{impure}^\circ fy k$ is encoded by $node^\circ (\text{inr} Y) fy k$.

By applying completion to the poset $\mathcal{L}^\circ F X$ with its definition order, we obtain an ACPO $\mathcal{L} F X$. The encodings of the functions $\text{impure}^\circ fy k$ are monotonic in $k$ and are completed to functions $\text{impure} fy k$ continuous in $k$. The function $\text{pure}^\circ$ is unchanged but, for notation consistency, we rename it into $\text{pure}$. The properties of completion ensure that, by hiding the details of how $itree F X \triangleq \mathcal{L} F X$ is built, interaction trees behave like the coinductive objects in Definition 8.