*This paper is an extended version of our previous work [AP21]: it simplifies the meta-theory, removes the reliance on general recursion for reinstalling interrupt handlers, adds state to reinstallable interrupt handlers, and extends the calculus with higher-order signal and interrupt payloads, and with dynamic process creation.

[a] [a,b]

# Higher-Order Asynchronous Effects*

Danel Ahman0000-0001-6595-2756  and  Matija Pretnar0000-0001-7755-2303
University of Ljubljana, Faculty of Mathematics and Physics, Jadranska 19,
Ljubljana, Slovenia<EMAIL_ADDRESS><EMAIL_ADDRESS>Institute of Mathematics, Physics and Mechanics, Jadranska 19, Ljubljana,
Slovenia

###### Abstract.

We explore asynchronous programming with algebraic effects. We complement
their conventional synchronous treatment by showing how to naturally also
accommodate asynchrony within them, namely, by decoupling the execution of
operation calls into signalling that an operation’s implementation needs to be
executed, and interrupting a running computation with the operation’s result,
to which the computation can react by installing interrupt handlers. We
formalise these ideas in a small core calculus and demonstrate its flexibility
using examples ranging from a multi-party web application, to pre-emptive
multi-threading, to (cancellable) remote function calls, to a parallel variant
of runners of algebraic effects. In addition, the paper is accompanied by a
formalisation of the calculus’s type safety proofs in Agda, and a prototype
implementation in OCaml.

###### Key words and phrases:

algebraic effects, asynchrony, concurrency, interrupt handling, signals,
promises

This project has received funding from the European Union’s Horizon 2020
research and innovation programme under the Marie Skłodowska-Curie grant
agreement No 834146  . This material is based upon work supported by the Air
Force Office of Scientific Research under awards number FA9550-17-1-0326 and
FA9550-21-1-0024.

##  1\. Introduction

Effectful programming abstractions are at the heart of many modern general-
purpose programming languages. They can increase expressiveness by giving
programmers access to first-class (delimited) continuations, but often they
simply help programmers to write cleaner code, e.g., by avoiding having to
manage a program’s memory explicitly in state-passing style, or getting lost
in callback hell while programming asynchronous computations.

An increasing number of language designers and programmers are starting to
embrace _algebraic effects_ , where one uses algebraic operations [PP02] and
effect handlers [PP13] to uniformly, modularly, and user-definably express a
wide range of effectful behaviour, ranging from basic examples such as state,
rollbacks, exceptions, and nondeterminism [BP15], to advanced applications in
concurrency [SDW+21] and statistical probabilistic programming [BCJ+19], and
even quantum computation [Sta15].

While covering many examples, the conventional treatment of algebraic effects
is _synchronous_ by nature. In it effects are invoked by placing operation
calls in one’s code, which then propagate outwards until they trigger the
actual effect, finally yielding a result to the rest of the computation that
has been _waiting_ in a blocked state the whole time. While blocking the
computation is indeed sometimes necessary, e.g., in the presence of general
effect handlers that can execute their continuation any number of times, it
forces all uses of algebraic effects to be synchronous, even when this is not
necessary, e.g., when the effect involves executing a remote query to which a
response is not needed (immediately).

Motivated by the recent interest in the combination of asynchrony and
algebraic effects [Lei17, SDW+21], in this paper we explore what it takes to
accompany the synchronous treatment of algebraic effects with an
_asynchronous_ one (in terms of language design, safe programming
abstractions, and a self-contained core calculus). At the heart of our
approach is the decoupling of the execution of algebraic operation calls into
(i) _signalling_ that some implementation of an operation needs to be
executed, and (ii) _interrupting_ a running computation with its result, to
which the computation can react by (iii) _installing interrupt handlers_.
Importantly, we show that our approach is flexible enough that not all signals
need to have a corresponding interrupt, and vice versa, allowing us to also
model _spontaneous behaviour_ , such as a user clicking a button or the
environment pre-empting a thread.

While we are not the first ones to work on asynchrony for algebraic effects,
the prior work in this area (in the context of general effect handlers) has
achieved it by simply _delegating_ the actual asynchrony to the respective
language backends [Lei17, SDW+21]. In contrast, in this paper we demonstrate
how to capture the combination of asynchrony and algebraic effects in a _self-
contained_ core calculus. It is important to emphasise that our aim is not to
replace general effect handlers, but instead to _complement_ them with robust
primitives tailored to asynchrony—as we highlight throughout the paper, our
proposed approach is algebraic by design, so as to be ready for future
extensions with general effect handlers.

##### Paper Structure

In Section 2, we give a high-level overview of our approach to asynchrony for
algebraic effects. In Sections 3 and 4, we recap our previous work [AP21] on
asynchronous algebraic effects using a core calculus, $\lambda_{\text{\ae}}$,
equipped with a small-step operational semantics and a type-and-effect system.
In Section 5, we explore extensions of $\lambda_{\text{\ae}}$ necessary to
accommodate reinstallable interrupt handlers, higher-order signal and
interrupt payloads, and the dynamic creation of processes, and prove their
type safety. In Section 6, we show how these extensions can be used in
examples such as pre-emptive multi-threading, remote function calls, and a
parallel variant of runners of algebraic effects, simplifying the examples in
our prior work [AP21]. We conclude by discussing related and future work in
Section 7.

##### Code

The paper is accompanied by a _formalisation_ of $\lambda_{\text{\ae}}$’s type
safety proofs in Agda [Ahm23], and a _prototype implementation_ of
$\lambda_{\text{\ae}}$ in OCaml, called Æff [Pre21].

In Agda, we consider only the well-typed syntax of a variant of
$\lambda_{\text{\ae}}$ in which the subtyping rule manifests as an explicit
coercion, so as to make working with de Bruijn indices less painful.
Meanwhile, the Æff implementation provides an interpreter and a simple
typechecker, but does not yet support inferring or checking effect
annotations. Æff also provides a web interface that allows users to
interactively click through their programs’ executions. It also comes with
implementations of all the examples we present in this paper.

Separately, Poulson [Pou20] has shown how to implement $\lambda_{\text{\ae}}$
in Frank [CLMM20].

##  2\. Asynchronous Effects, by Example

We begin with a high-level overview of how we model asynchrony within
algebraic effects.

###  2.1. Conventional Algebraic Effects Are Synchronous by Nature

We first recall the basic ideas of programming with algebraic effects,
illustrating that their traditional treatment is synchronous by nature. For an
in-depth overview, we refer the reader to a tutorial on effect handlers
[Pre15], and to the seminal papers of the field [PP02, PP13].

In this algebraic treatment, sources of computational effects are modelled
using signatures of _operation symbols_ $\mathsf{op}:A_{\mathsf{op}}\to
B_{\mathsf{op}}$. For instance, one models $S$-valued state using operations
$\mathsf{get}:\mathsf{1}\to S$ and $\mathsf{set}:S\to\mathsf{1}$, and
$E$-valued exceptions using a single operation
$\mathsf{raise}:E\to\mathsf{0}$.

Programmers can then invoke the effect that an operation
$\mathsf{op}:A_{\mathsf{op}}\to B_{\mathsf{op}}$ models by placing an
_operation call_ $\mathsf{op}\;(V,y.M)$ in their code. Here, the parameter
value $V$ has type $A_{\mathsf{op}}$, and the variable $y$, which is bound in
the continuation $M$, has type $B_{\mathsf{op}}$. For instance, for the
$\mathsf{set}$ operation, the parameter value $V$ would be the new value of
the store, and for the $\mathsf{get}$ operation, the variable $y$ would be
bound to the current value of the store.

A program written in terms of operation calls is by itself just an inert piece
of code. To execute it, programmers have to provide _implementations_ for the
operation calls appearing in it. The idea is that an implementation of
$\mathsf{op}\;(V,y.M)$ takes $V$ as its input, and its output gets bound to
$y$. For instance, this could take the form of defining a suitable effect
handler [PP13], but could also be given by calls to runners of algebraic
effects [AB20], or simply by invoking some (default) top-level (native)
implementation. What is important is that some pre-defined piece of code
$M_{\mathsf{op}}[V/x]$ gets executed in place of every operation call
$\mathsf{op}\;(V,y.M)$.

Now, what makes the conventional treatment of algebraic effects _synchronous_
is that the execution of an operation call $\mathsf{op}\;(V,y.M)$ _blocks_
until some implementation of $\mathsf{op}$ returns a value $W$ to be bound to
$y$, so that the execution of the continuation $M[W/y]$ could proceed [KLO13,
BP14]. Conceptually, this kind of blocking behaviour can be illustrated as

$\begin{gathered}\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
8.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 25.28984pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{M_{\mathsf{op}}[V/x]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
78.47604pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-3.65875pt\hbox{$\scriptstyle{\mbox{\Large{$\leadsto^{\\!*}$}}}$}}}}}\ignorespaces{}{\hbox{\kern
96.69087pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
5.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,W\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
121.57977pt\raise-15.50003pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx<EMAIL_ADDRESS>0.0pt\raise 0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{\dots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
8.05pt\raise-28.00003pt\hbox{\hbox{\kern
0.0pt\raise-2.72075pt\hbox{$\scriptstyle{\mbox{\Large{$\leadsto$}}}$}}}}}\ignorespaces{}{\hbox{\kern
21.25002pt\raise-28.00003pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{\mathsf{op}\;(V,y.M)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
52.47104pt\raise-7.5pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
96.19208pt\raise-28.00003pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{M[W/y]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces{\hbox{\kern
145.76747pt\raise-28.00003pt\hbox{\hbox{\kern
0.0pt\raise-2.72075pt\hbox{$\scriptstyle{\mbox{\Large{$\leadsto$}}}$}}}}}\ignorespaces{}{\hbox{\kern
159.46748pt\raise-28.00003pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 5.0pt\raise
0.0pt\hbox{$\textstyle{\dots}$}}}}}}}\ignorespaces}}}}\ignorespaces\end{gathered}$
(1)

where
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,W$
is a computation that causes no effects and simply returns the value $W$.

While blocking the execution of the rest of the computation is needed in the
presence of general effect handlers that can execute their continuation any
number of times, e.g., when simulating nondeterminism [PP13], it forces all
uses of algebraic effects to be synchronous, even when this is not necessary,
e.g., when the effect in question involves executing a remote query to which a
response is not needed immediately, or sometimes never at all.

In the rest of this section, we describe how we decouple the invocation of an
operation call from the act of receiving its result, and how we give
programmers a means to block execution only when it is necessary. While we end
up surrendering some of effect handlers’ generality, such as having access to
the continuation that captures the rest of the computation to be handled, then
in return we get a natural and robust formalism for asynchronous programming.

###  2.2. Outgoing Signals and Incoming Interrupts

We begin by observing that the execution of an operation call
$\mathsf{op}\;(V,y.M)$, as depicted in (1), consists of _three distinct
phases_ : (i) signalling that an implementation of $\mathsf{op}$ needs to be
executed with parameter $V$ (the up-arrow), (ii) executing this implementation
(the horizontal arrow), and (iii) interrupting the blocked computation $M$
with a value $W$ (the down-arrow). In order to overcome the unwanted side-
effects of blocking execution at every operation call, we decouple these
phases into separate programming concepts, allowing $M$ to proceed executing
even if (ii) has not yet completed and (iii) taken place. In particular, we
decouple an operation call into issuing an _outgoing signal_ , written
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{\mathsf{op}}\,(V,M)$,
and receiving an _incoming interrupt_ , written
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{\mathsf{op}}\,(W,M)$.

It is important to note that while we have used the execution of operation
calls to motivate the introduction of signals and interrupts as programming
concepts, _not all issued signals need to have a corresponding interrupt
response_ , and _not all interrupts need to be responses to issued signals_ ,
allowing us to also model spontaneous behaviour, such as a user clicking a
button or the environment pre-empting a thread.

When _issuing a signal_
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{\mathsf{op}}\,(V,M)$,
the value $V$ is called a _payload_ , such as a location to be looked up or a
message to be displayed, aimed at whoever is listening for the given signal.
We use the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}$-notation
to indicate that signals issued in sub-computations propagate outwards—in this
sense signals behave just like conventional algebraic operation calls.
Crucially however, these outgoing signals differ from conventional algebraic
operation calls in that no additional variables are bound in the continuation
$M$, making it naturally possible to continue executing $M$ straight after the
signal has been issued, as depicted below:

$\textstyle{\dots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\leadsto$$\textstyle{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,M)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{op}\,V}$$\leadsto$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\leadsto$$\textstyle{\dots}$

As a _running example_ , let us consider a computation
$M_{\text{feedClient}}$, which lets a user scroll through a seemingly infinite
feed of data, e.g., by repeatedly clicking a “next page” button. For
efficiency, $M_{\text{feedClient}}$ does not initially cache all the data
available on a server, but instead requests a new batch of data each time
scrolling through the data is nearing the end of the cache. To communicate
with the outside world, $M_{\text{feedClient}}$ can issue a signal

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{\mathsf{request}}\,(\mathit{cachedSize}+1,M_{\text{feedClient}})$

to request a new batch of data starting from the end of the current cache, or
a different signal

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{\mathsf{display}}\,(\mathit{message},M_{\text{feedClient}})$

to display a string $\mathit{message}$ to the user. In both cases, the
continuation _does not wait_ for an acknowledgement that the signal was
received, but instead continues to provide a seamless experience to the user.
It is however worth noting that these signals differ in what
$M_{\text{feedClient}}$ expects of them: to the $\mathsf{request}$ signal, it
expects a response at some future point in its execution, while it does not
expect any response to the $\mathsf{display}$ signal, illustrating that not
every issued signal needs an immediate response, and that some do not need one
at all.

When the outside world wants to get the attention of a computation, be it in
response to a signal or spontaneously, it happens by _propagating an
interrupt_
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{\mathsf{op}}\,(W,M)$
to the computation. Here, the value $W$ is again called a _payload_ , while
$M$ is the computation receiving the interrupt. It is important to note that
unlike signals, interrupts are not triggered by the computation itself, but
are instead issued by the _outside world_ , and can thus interrupt any
sequence of evaluation steps, e.g., as depicted in

$\scriptstyle{\mathsf{op}\,W}$$\textstyle{\dots\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\leadsto$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\leadsto$$\textstyle{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(W,M)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\leadsto$$\textstyle{\dots}$

In our running example, there are two interrupts of interest that
$M_{\text{feedClient}}$ might receive:

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{\mathsf{response}}\,(\mathit{newBatch},M)$

which delivers a batch of new data to replenish $M_{\text{feedClient}}$’s
cache, and

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{\mathsf{nextItem}}\,((),M)$

with which the user requests to see the next data item. In both cases, the
continuation $M$ represents the state of $M_{\text{feedClient}}$ at the time
of receiving the interrupt.

We use the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}$-notation
to indicate that interrupts propagate inwards into sub-computations, trying to
reach anyone listening for them, and only get discarded when they reach a
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}$.
Programmers are not expected to write interrupts explicitly in their
programs—instead, interrupts are usually induced by signals issued by other
parallel processes, as explained next.

###  2.3. A Signal for the Sender Is an Interrupt to the Receiver

As noted above, the computations we consider do not evolve in isolation,
instead they also communicate with the outside world, by issuing outgoing
signals and receiving incoming interrupts.

We model the outside world by composing individual computations into _parallel
processes_ $P,Q,\ldots$. To keep the presentation clean and focussed on the
asynchrony of algebraic effects, we consider a very simple model of
parallelism: a process is either one of the computations being run in
parallel, written
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M$,
or the parallel composition of two processes, written
$P\mathbin{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}||}}Q$.
Later, in Section 5.4, we show how to also accommodate dynamic process
creation.

To capture the signals and interrupts based interaction of processes, our
operational semantics includes rules for _propagating outgoing signals_ from
individual computations to processes, _turning processes’ outgoing signals
into incoming interrupts_ for their surrounding world, and _propagating
incoming interrupts_ from processes to individual computations. For instance,
in our running example, $M_{\text{feedClient}}$’s request for new data is
executed as follows:

$\begin{array}[]{r l}&\leavevmode\hbox to121.12pt{\vbox
to14.69pt{\pgfpicture\makeatletter\hbox{\hskip 60.55855pt\lower-7.34602pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{56.55855pt}{7.34602pt}\pgfsys@lineto{-56.55855pt}{7.34602pt}\pgfsys@curveto{-58.76772pt}{7.34602pt}{-60.55855pt}{5.55519pt}{-60.55855pt}{3.34602pt}\pgfsys@lineto{-60.55855pt}{-3.34602pt}\pgfsys@curveto{-60.55855pt}{-5.55519pt}{-58.76772pt}{-7.34602pt}{-56.55855pt}{-7.34602pt}\pgfsys@lineto{56.55855pt}{-7.34602pt}\pgfsys@curveto{58.76772pt}{-7.34602pt}{60.55855pt}{-5.55519pt}{60.55855pt}{-3.34602pt}\pgfsys@lineto{60.55855pt}{3.34602pt}\pgfsys@curveto{60.55855pt}{5.55519pt}{58.76772pt}{7.34602pt}{56.55855pt}{7.34602pt}\pgfsys@closepath\pgfsys@moveto{-60.55855pt}{-7.34602pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-59.70497pt}{-3.99245pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{request}\,(V,\leavevmode\hbox
to37.08pt{\vbox to10.48pt{\pgfpicture\makeatletter\hbox{\hskip
18.53831pt\lower-5.24245pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{14.53831pt}{5.24245pt}\pgfsys@lineto{-14.53831pt}{5.24245pt}\pgfsys@curveto{-16.74748pt}{5.24245pt}{-18.53831pt}{3.45161pt}{-18.53831pt}{1.24245pt}\pgfsys@lineto{-18.53831pt}{-1.24245pt}\pgfsys@curveto{-18.53831pt}{-3.45161pt}{-16.74748pt}{-5.24245pt}{-14.53831pt}{-5.24245pt}\pgfsys@lineto{14.53831pt}{-5.24245pt}\pgfsys@curveto{16.74748pt}{-5.24245pt}{18.53831pt}{-3.45161pt}{18.53831pt}{-1.24245pt}\pgfsys@lineto{18.53831pt}{1.24245pt}\pgfsys@curveto{18.53831pt}{3.45161pt}{16.74748pt}{5.24245pt}{14.53831pt}{5.24245pt}\pgfsys@closepath\pgfsys@moveto{-18.53831pt}{-5.24245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.68474pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$M_{\text{feedClient}}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}))$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\mathbin{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}||}}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M_{\text{feedServer}}\\\\[2.15277pt]
\leadsto&\leavevmode\hbox to182.05pt{\vbox
to14.69pt{\pgfpicture\makeatletter\hbox{\hskip 91.0263pt\lower-7.34602pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{87.0263pt}{7.34602pt}\pgfsys@lineto{-87.0263pt}{7.34602pt}\pgfsys@curveto{-89.23547pt}{7.34602pt}{-91.0263pt}{5.55519pt}{-91.0263pt}{3.34602pt}\pgfsys@lineto{-91.0263pt}{-3.34602pt}\pgfsys@curveto{-91.0263pt}{-5.55519pt}{-89.23547pt}{-7.34602pt}{-87.0263pt}{-7.34602pt}\pgfsys@lineto{87.0263pt}{-7.34602pt}\pgfsys@curveto{89.23547pt}{-7.34602pt}{91.0263pt}{-5.55519pt}{91.0263pt}{-3.34602pt}\pgfsys@lineto{91.0263pt}{3.34602pt}\pgfsys@curveto{91.0263pt}{5.55519pt}{89.23547pt}{7.34602pt}{87.0263pt}{7.34602pt}\pgfsys@closepath\pgfsys@moveto{-91.0263pt}{-7.34602pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-90.17273pt}{-3.99245pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{request}\,(V,\leavevmode\hbox
to54.88pt{\vbox to10.48pt{\pgfpicture\makeatletter\hbox{\hskip
27.44107pt\lower-5.24245pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{23.44107pt}{5.24245pt}\pgfsys@lineto{-23.44107pt}{5.24245pt}\pgfsys@curveto{-25.65024pt}{5.24245pt}{-27.44107pt}{3.45161pt}{-27.44107pt}{1.24245pt}\pgfsys@lineto{-27.44107pt}{-1.24245pt}\pgfsys@curveto{-27.44107pt}{-3.45161pt}{-25.65024pt}{-5.24245pt}{-23.44107pt}{-5.24245pt}\pgfsys@lineto{23.44107pt}{-5.24245pt}\pgfsys@curveto{25.65024pt}{-5.24245pt}{27.44107pt}{-3.45161pt}{27.44107pt}{-1.24245pt}\pgfsys@lineto{27.44107pt}{1.24245pt}\pgfsys@curveto{27.44107pt}{3.45161pt}{25.65024pt}{5.24245pt}{23.44107pt}{5.24245pt}\pgfsys@closepath\pgfsys@moveto{-27.44107pt}{-5.24245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.5875pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M_{\text{feedClient}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}))\mathbin{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}||}}\leavevmode\hbox
to55.38pt{\vbox to10.48pt{\pgfpicture\makeatletter\hbox{\hskip
27.68997pt\lower-5.24245pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{23.68997pt}{5.24245pt}\pgfsys@lineto{-23.68997pt}{5.24245pt}\pgfsys@curveto{-25.89914pt}{5.24245pt}{-27.68997pt}{3.45161pt}{-27.68997pt}{1.24245pt}\pgfsys@lineto{-27.68997pt}{-1.24245pt}\pgfsys@curveto{-27.68997pt}{-3.45161pt}{-25.89914pt}{-5.24245pt}{-23.68997pt}{-5.24245pt}\pgfsys@lineto{23.68997pt}{-5.24245pt}\pgfsys@curveto{25.89914pt}{-5.24245pt}{27.68997pt}{-3.45161pt}{27.68997pt}{-1.24245pt}\pgfsys@lineto{27.68997pt}{1.24245pt}\pgfsys@curveto{27.68997pt}{3.45161pt}{25.89914pt}{5.24245pt}{23.68997pt}{5.24245pt}\pgfsys@closepath\pgfsys@moveto{-27.68997pt}{-5.24245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-26.8364pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M_{\text{feedServer}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leadsto&\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{request}\,\big{(}V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M_{\text{feedClient}}\mathbin{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}||}}\leavevmode\hbox
to113.84pt{\vbox to14.69pt{\pgfpicture\makeatletter\hbox{\hskip
56.91853pt\lower-7.34602pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{52.91853pt}{7.34602pt}\pgfsys@lineto{-52.91853pt}{7.34602pt}\pgfsys@curveto{-55.1277pt}{7.34602pt}{-56.91853pt}{5.55519pt}{-56.91853pt}{3.34602pt}\pgfsys@lineto{-56.91853pt}{-3.34602pt}\pgfsys@curveto{-56.91853pt}{-5.55519pt}{-55.1277pt}{-7.34602pt}{-52.91853pt}{-7.34602pt}\pgfsys@lineto{52.91853pt}{-7.34602pt}\pgfsys@curveto{55.1277pt}{-7.34602pt}{56.91853pt}{-5.55519pt}{56.91853pt}{-3.34602pt}\pgfsys@lineto{56.91853pt}{3.34602pt}\pgfsys@curveto{56.91853pt}{5.55519pt}{55.1277pt}{7.34602pt}{52.91853pt}{7.34602pt}\pgfsys@closepath\pgfsys@moveto{-56.91853pt}{-7.34602pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-56.06496pt}{-3.99245pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{request}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;\leavevmode\hbox
to37.57pt{\vbox to10.48pt{\pgfpicture\makeatletter\hbox{\hskip
18.7872pt\lower-5.24245pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{14.7872pt}{5.24245pt}\pgfsys@lineto{-14.7872pt}{5.24245pt}\pgfsys@curveto{-16.99637pt}{5.24245pt}{-18.7872pt}{3.45161pt}{-18.7872pt}{1.24245pt}\pgfsys@lineto{-18.7872pt}{-1.24245pt}\pgfsys@curveto{-18.7872pt}{-3.45161pt}{-16.99637pt}{-5.24245pt}{-14.7872pt}{-5.24245pt}\pgfsys@lineto{14.7872pt}{-5.24245pt}\pgfsys@curveto{16.99637pt}{-5.24245pt}{18.7872pt}{-3.45161pt}{18.7872pt}{-1.24245pt}\pgfsys@lineto{18.7872pt}{1.24245pt}\pgfsys@curveto{18.7872pt}{3.45161pt}{16.99637pt}{5.24245pt}{14.7872pt}{5.24245pt}\pgfsys@closepath\pgfsys@moveto{-18.7872pt}{-5.24245pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-17.93362pt}{-2.44444pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$M_{\text{feedServer}}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\big{)}\\\\[2.15277pt]
\leadsto&\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{request}\,\big{(}V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;M_{\text{feedClient}}\mathbin{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}||}}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}run}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{request}\,(V,M_{\text{feedServer}}))\big{)}\end{array}$

Here, the first and the last reduction step respectively propagate signals
outwards and interrupts inwards. The middle reduction step corresponds to what
we call a _broadcast rule_ —it turns an outward moving signal in one of the
processes into an inward moving interrupt for the process parallel to it,
while continuing to propagate the signal outwards to any further parallel
processes. The active redexes in these rules are highlighted in grey.

###  2.4. Promising To Handle Interrupts

So far, we have shown that our computations can issue outgoing signals and
receive incoming interrupts, and how these evolve and get communicated when
executing parallel processes, but we have not yet said anything about how
computations can actually _react_ to incoming interrupts of interest.

In order to react to interrupts, our computations can install _interrupt
handlers_ , written

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$

that should be read as: “we promise to handle a future incoming interrupt
named $\mathsf{op}$ using the computation $M$ in the continuation $N$, with
$x$ bound to the payload of the interrupt”. Fulfilling this promise consists
of executing $M$ and binding its result to the variable $p$ in $N$, as
captured by the following reduction rule:

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M[V/x]\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$

It is worth noting that the interrupt itself _keeps propagating inwards_ into
the sub-computation $N$. In order to skip certain interrupt handlers for some
$\mathsf{op}$, one can carry additional data in $\mathsf{op}$’s payload (e.g.,
a thread ID) and then condition the (non-)triggering of those interrupt
handlers on this data, e.g., as we demonstrate in Section 6.1.

Interrupts that do not match a given interrupt handler
($\mathsf{op}\neq\mathsf{op}^{\prime}$) simply move past it:

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op^{\prime}}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op^{\prime}}\,(V,N)$

Interrupt handlers differ from conventional algebraic operation calls (see
Section 2.1) in two important aspects. First, they enable _user-side post-
processing_ of received data, using $M$, while in operation calls the result
is immediately bound in the continuation. Second, and more importantly, their
semantics is _non-blocking_. In particular, we have a congruence rule

$N\leadsto
N^{\prime}\qquad\text{implies}\qquad\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N^{\prime}$

meaning that the continuation $N$, and thus the whole computation, can make
progress even though no interrupt $\mathsf{op}$ has been propagated to the
computation from the outside world.

As the observant reader might have noticed, the non-blocking behaviour of
interrupt handling means that our operational semantics has to work on _open
terms_ because the variable $p$ can appear free in both $N$ and $N^{\prime}$
in the congruence rule given above. However, it is important to note that $p$
is not an arbitrarily typed variable, but in fact gets assigned a
distinguished _promise type_ $\langle X\rangle$ for some value type $X$—we
shall crucially make use of this typing of $p$ in the proof of type safety for
our $\lambda_{\text{\ae}}$-calculus (see 2 and 7).

###  2.5. Blocking on Interrupts Only When Necessary

As noted earlier, installing an interrupt handler means making a promise to
handle a given interrupt in the future. To check that an interrupt has been
received and handled, we provide programmers a means to selectively _block
execution_ and _await_ a specific promise to be fulfilled, written
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M$,
where if $V$ has a promise type $\langle X\rangle$, the variable $x$ bound in
$M$ has type $X$. Importantly, the continuation $M$ is executed only when the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
is handed a _fulfilled promise_ $\langle V\rangle$, as

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;\langle
V\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M\leadsto
M[V/x]$

In our example of scrolling through a seemingly infinite feed,
$M_{\text{feedClient}}$ could use
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
to block until it has received an initial configuration, such as the batch
size used by $M_{\text{feedServer}}$.

As the terminology suggests, this part of $\lambda_{\text{\ae}}$ is strongly
influenced by existing work on _futures and promises_ [Sch02] for structuring
concurrent programs, and their use in modern languages, such as in Scala
[HPM+20]. While prior work often models promises as writeable, single-
assignment references, we instead use the substitution of values for ordinary
immutable variables (of distinguished promise type) to model that a promise
gets fulfilled exactly once.

###  2.6. Reinstalling Interrupt Handlers

As seen in the reduction rule

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M[V/x]\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$

the interrupt handler is _not reinstalled by default_. The programmers can
selectively reinstall interrupt handlers using general recursion [AP21], or
use the extension of $\lambda_{\text{\ae}}$ with _reinstallable interrupt
handlers_ we propose in this paper (see Section 5.1), which have the form

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$

These behave similarly to ordinary interrupt handlers, except that the
handling computation $M$ has access to an additional variable $r$ bound to a
function that reinstalls the handler when called. Specifically, triggering a
reinstallable interrupt handler has the following form:

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)\\\
\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M\big{[}V/x,\big{(}{\mathop{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}fun}}}\;\\_\mapsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,p\big{)}/r\big{]}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$

In examples, we often find it useful to also pass some data between subsequent
reinstalls of an interrupt handler. Programmers can achieve this by working
with an additionally assumed primitive notion of memory references [AP21], or
by using a _stateful variant of reinstallable interrupt handlers_ that we
propose in this paper. The latter have the form

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\,s\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}@}_{S}\;W\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$

where $S$ is the type of state associated with a particular interrupt handler,
$W$ is the interrupt handler’s state at the time of its next triggering, the
variable $s$ gives the interrupt handler code $M$ access to the state, and the
state can be updated by reinstalling the handler with an updated value using
$r$. Specifically, the interrupt handler triggering rule now has the form

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\,s\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}@}_{S}\;W\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M\big{[}V/x,R/r,W/s\big{]}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$

where $R$ denotes a function that reinstalls the interrupt handler with an
updated state value:

$R~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}{\mathop{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}fun}}}\;(s^{\prime}\mathinner{:}S)\mapsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\,s\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}@}_{S}\;s^{\prime}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,p$

When it is clear from the context, for brevity we often omit the
$S$-annotation in examples.

###  2.7. Putting It All Together

We conclude this overview by showing how to implement the example of a user
scrolling through a seemingly infinite feed of data in our
$\lambda_{\text{\ae}}$-calculus.

For a simpler exposition, we allow ourselves access to mutable references,
with which we communicate data between different interrupt handlers, though
the same can be achieved by rolling one’s own state. For passing data between
subsequent reinstalls of the same interrupt handler, we use the state-passing
features of interrupt handlers introduced above.

While having explicit continuations in operation calls, signals, interrupt
handlers, and when awaiting promises to be fulfilled makes the meta-theory of
the underlying calculus cleaner, in programming we prefer to use _generic_
versions of them, i.e., ones with trivial continuations [PP03]. In particular,
we define and use the following syntactic sugar:

$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,V$
$\displaystyle~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,())$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\mapsto
M)$ $\displaystyle~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,p$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\,s\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}@}\;V$
$\displaystyle~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\,r\,s\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}@}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,p$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V$
$\displaystyle~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,x$

####  2.7.1. Client

We implement the client computation $M_{\text{feedClient}}$ as the function
feedClient defined below. For presentation purposes, we split its definition
between multiple code blocks.

First, the client initialises some auxiliary references, issues a signal to
the server to ask for the data batch size that it uses, and then installs a
corresponding interrupt handler:

⬇

let feedClient () =

let cachedData = ref [] in

let requestInProgress = ref false in

send batchSizeRequest ();

let batchSizePromise = promise (batchSizeResponse batchSize |-> return
<<batchSize>>) in

…

While the server is asynchronously responding to the batch size request, the
client sets up an auxiliary function requestNewData, with which it can request
new data from the server:

⬇

…

let requestNewData offset =

requestInProgress := true;

send request offset;

promise (response newBatch |->

cachedData := !cachedData @ newBatch;

requestInProgress := false;

return <<()>>

)

in

…

Here, we first set a flag indicating that a new data request is in process,
then issue a request signal to the server, and finally install an interrupt
handler that updates the cache once a corresponding response interrupt
arrives. We note that the client computation does not block while awaiting new
data from the server—instead, it continues executing, notifying the user to
wait and try again once the cache temporarily becomes empty (see below).

As a last step of setting itself up, the client blocks until the server has
responded with the batch size it uses by awaiting batchSizePromise to be
fulfilled, after which the client starts its main loop, which we implement as
a simple reinstallable interrupt handler:

⬇

…

let batchSize = await batchSizePromise in

promise (nextItem _ r currentItem |->

let cachedSize = length !cachedData in

(if (currentItem > cachedSize - batchSize / 2) && (not !requestInProgress)
then

requestNewData (cachedSize + 1)

else

return ());

if currentItem < cachedSize then

send display (toString (nth !cachedData currentItem));

r (currentItem + 1)

else

send display "please wait a bit and try again";

r currentItem

) @ 0

In it, the client listens for nextItem interrupts from the user to display
more data. Once the interrupt arrives, the client checks if its cache is
becoming empty—if so, it uses the requestNewData function to request more data
from the server. Next, if there is still some data in the cache, the client
issues a signal to display the next data item to the user. If however the
cache is empty, the client issues a signal to display a message asking the
user to wait. The client then simply reinvokes itself by reinstalling the
interrupt handler for nextItem interrupts. Observe that the currentItem
counter is initially set to $0$ and then passed between subsequent interrupt
handler reinstalls using the state-passing features introduced earlier.

####  2.7.2. Server

We implement the server computation $M_{\text{feedServer}}$ as the following
function:

⬇

let feedServer batchSize =

promise (batchSizeRequest () r |->

send batchSizeResponse batchSize;

r ()

);

promise (request offset r |->

let payload = map (fun x |-> 10 * x) (range offset (offset + batchSize - 1))
in

send response payload;

r ()

)

where the computation range i j returns a list of integers ranging from i to j
(both inclusive).

The server simply installs two reinstallable interrupt handlers: the first one
listens for and responds to client’s requests about the batch size it uses;
and the second one responds to client’s requests for new data. Both interrupt
handlers then simply reinstall themselves.

####  2.7.3. User

We can also simulate the user as a computation. For the sake of simplicity, we
allow ourselves general recursion to implement the user behaviour as an
infinite loop that every now and then issues a request to the client to
display the next data item.

⬇

let rec user () =

let rec wait n =

if n = 0 then return () else wait (n - 1)

in

send nextItem (); wait 10; user ()

Alternatively, without assuming general recursion, we could have implemented
the user instead as two parallel processes that indefinitely ping-pong each
other, and occasionally issue nextItem signals to the client (see Section 7
for an example of such non-terminating behaviour). It is also straightforward
to extend the user program with a reinstallable handler for display interrupts
that simulates displaying the data items received from the client (omitted
here).

####  2.7.4. Running the Server, Client, and User in Parallel

Finally, we can simulate our running example in full by running all three
computations as parallel processes, as follows:

⬇

run (feedServer 42) || run (feedClient ()) || run (user ())

##  3\. A Calculus for Asynchronous Effects: Values and Computations

Before we focus on extensions necessary for higher-order asynchronous effects
in Section 5, we first recap $\lambda_{\text{\ae}}$, our existing core
calculus for programming with first-order asynchronous effects [AP21]. The
version we present here differs from the previous one in two aspects: we drop
the reliance on general recursion, as reinstallable interrupt handlers that we
introduce in Section 5.1 are sufficient to express all the existing examples,
and we slightly modify the behaviour of the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
construct in order to make the meta-theory slightly simpler.

To better explain the different features of the calculus and its semantics, we
split the recap of $\lambda_{\text{\ae}}$ into a _sequential_ part (discussed
below) and a _parallel_ part (discussed in Section 4).

###  3.1. Values and Computations

We base $\lambda_{\text{\ae}}$ on the fine-grain call-by-value
$\lambda$-calculus (FGCBV) [LPT03], and as such, it is a low-level
intermediate language to which a corresponding high-level user-facing
programming language could be compiled to—this is what happens in our
prototype implementation [Pre21].

The syntax of terms is given in Figure 1, stratified into _values_ and
_computations_ , as in FGCBV. While we do not study effect inference in this
paper, we equip certain terms with type annotations that in our experience
should make it possible to fully infer types.

Values $\displaystyle V,W\mathrel{\;{:}{:}{=}\ }$ $\displaystyle x$ variable
$\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle()\mathrel{\,\;\big{|}\ \ \\!}\\!(V,W)$ unit and pairing
$\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inl}_{Y}\,V\mathrel{\,\;\big{|}\
\
\\!}\\!\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inr}_{X}\,V$
left and right injections $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle{\mathop{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}fun}}}\;(x:X)\mapsto
M$ function abstraction $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\langle V\rangle$ fulfilled promise Computations $\displaystyle
M,N\mathrel{\;{:}{:}{=}\ }$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,V$
returning a value $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=M\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$
sequencing $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$ $\displaystyle V\,W$
function application $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{(x,y)\mapsto
M\\}$ product elimination $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{\\}_{Z\and(o,\iota)}$
empty elimination $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inl}\,x\mapsto
M,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inr}\,y\mapsto
N\\}$ sum elimination $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,M)$
outgoing signal $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M)$
incoming interrupt $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$
interrupt handler $\displaystyle\mathrel{\,\;\big{|}\ \ \\!}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M$
awaiting a promise to be fulfilled

Figure 1. Values and Computations.

##### Values

The values $V,W,\ldots$ are mostly standard. They include variables,
introduction forms for sums and products, and functions. The only
$\lambda_{\text{\ae}}$-specific value is $\langle V\rangle$, which denotes a
_fulfilled promise_ , indicating that the promise of handling some interrupt
has been fulfilled with the value $V$.

##### Computations

The computations $M,N,\ldots$ also include all standard terms from FGCBV:
returning values, sequencing, function application, and elimination forms.

The first two $\lambda_{\text{\ae}}$-specific computations are _signals_
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,M)$
and _interrupts_
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M)$,
where $\mathsf{op}$ is drawn from a set $\Sigma$ of names, $V$ is a data
payload, and $M$ is a continuation.

The next $\lambda_{\text{\ae}}$-specific computation is the _interrupt
handler_
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$,
where $x$ is bound in $M$ and $p$ in $N$. As discussed in the previous
section, one should understand this computation as making a promise to handle
a future incoming interrupt $\mathsf{op}$ by executing the computation $M$.
Sub-computations of the continuation $N$ can then explicitly await, when
necessary, for this promise to be fulfilled by blocking on the _promise-typed
variable_ $p$ using the final $\lambda_{\text{\ae}}$-specific computation
term, the _awaiting_ construct
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M$.
It is useful to note that the $p$ used above is an ordinary variable—it just
gets assigned the distinguished promise type $\langle X\rangle$ by the
interrupt handler (as discussed in Section 3.3).

###  3.2. Small-Step Operational Semantics

We equip $\lambda_{\text{\ae}}$ with an evaluation contexts based small-step
operational semantics, defined using a reduction relation $M\leadsto N$. The
_reduction rules_ and _evaluation contexts_ are given in Figure 2. We discuss
the rules in detail below.

Standard computation rules
$\displaystyle({\mathop{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}fun}}}\;(x\mathinner{:}X)\mapsto
M)\,V$ $\displaystyle\leadsto M[V/x]$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,V)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$
$\displaystyle\leadsto N[V/x]$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;(V,W)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{(x,y)\mapsto
M\\}$ $\displaystyle\leadsto M[V/x,W/y]$
$\displaystyle\mathllap{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inl}_{Y}\,V)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inl}\,x\mapsto
M,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inr}\,y\mapsto
N\\}}$ $\displaystyle\leadsto M[V/x]$
$\displaystyle\mathllap{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}match}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inr}_{X}\,W)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}with}\;\\{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inl}\,x\mapsto
M,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}inr}\,y\mapsto
N\\}}$ $\displaystyle\leadsto N[W/y]$ Algebraicity of signals, interrupt
handlers, and awaiting
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,M))\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=M\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;y\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N_{1})\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N_{2}$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;y\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=N_{1}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N_{2})$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
y\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;V\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
y\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=M\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$
Commutativity of signals with interrupt handlers
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(V,N)$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$
Interrupt propagation
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,W)$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,W$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(W,M))$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(W,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M))$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M[V/x]\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op^{\prime}}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op^{\prime}}\,(V,N)\;\;\;{\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}(\mathsf{op}\neq\mathsf{op}^{\prime})}$
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;W\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M)$
$\displaystyle\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;W\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M)$
Awaiting a promise to be fulfilled
$\displaystyle\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;\langle
V\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M$
$\displaystyle\leadsto M[V/x]$

Evaluation context rule
$\displaystyle\inferrule*[Lab={\color[rgb]{0.5,0.5,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.5,0.5}}]{M\leadsto
N}{\mathcal{E}[M]\leadsto\mathcal{E}[N]}$ where
$\displaystyle\text{$\mathcal{E}$}\mathrel{\;{:}{:}{=}\
}[~{}]\mathrel{\,\;\big{|}\ \
\\!}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;x=\mathcal{E}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N\mathrel{\,\;\big{|}\
\
\\!}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op}\,(V,\mathcal{E})\mathrel{\,\;\big{|}\
\
\\!}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathcal{E})\mathrel{\,\;\big{|}\
\
\\!}\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathcal{E}$

Figure 2. Small-step Operational Semantics of Computations.

##### Computation Rules

The first group includes _standard reduction rules_ from FGCBV, such as
$\beta$-reducing function applications, sequential composition, and the
standard elimination forms. These rules involve standard _capture avoiding
substitutions_ $V[W/x]$ and $M[W/x]$, defined by straightforward mutual
structural recursion.

##### Algebraicity

This group of reduction rules _propagates outwards_ the signals that have been
issued, interrupt handlers that have been installed, and computations awaiting
fulfilled promises. While it is not surprising that outgoing signals behave
like algebraic _operation calls_ , getting propagated outwards as far as
possible, then it is much more curious that the natural operational behaviour
of interrupt handlers turns out to be the same. As we shall explain in Section
7, despite using the (operating systems inspired) “handler” terminology,
mathematically interrupt handlers are in fact a form of scoped algebraic
operations [PSWJ18].

In contrast to our original calculus [AP21], the awaiting construct also
propagates outwards. Before, awaiting a promise in any subcomputation would
block the evaluation immediately, whereas now, we can do the additional
outwards propagation steps. Importantly, this does not significantly change
the computational behaviour, as after the propagation, the evaluation still
blocks as long as the promise is left unfulfilled. The main difference and
benefit is that all computations awaiting for a promise variable $p$ now show
this explicitly at their top-level, as they are of the form
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
x\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M$.
This change significantly simplifies the normal forms of computations (see
Section 3.4) and the resulting meta-theory.

##### Commutativity of Signals With Interrupt Handlers

This rule complements the algebraicity rule for signals, by further
propagating them outwards, past any enveloping interrupt handlers. From the
perspective of algebraic effects, this rule is an example of two algebraic
operations _commuting_ [HPP06]. For this rule to be type safe, the type system
ensures that the (promise-typed) variable $p$ cannot appear in the payload
value $V$.

##### Interrupt Propagation

The handler-operation curiosity does not end with interrupt handlers. This
group of reduction rules describes how interrupts are _propagated inwards_
into sub-computations. While
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M)$
might look like a conventional operation call, then its operational behaviour
instead mirrors that of (deep) _effect handling_ , where one also recursively
descends into the computation being handled. The first reduction rule states
that we can safely discard an interrupt when it reaches a trivial, effect-free
computation
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}return}\,W$.
The second rule states that we can propagate incoming interrupts past any
outward moving signals. The next two rules describe how interrupts interact
with interrupt handlers, in particular, that the former behave like effect
handling (when understanding interrupt handlers as generalised algebraic
operations). On the one hand, if the interrupt matches the interrupt handler
it encounters, the corresponding handler code $M$ is executed, and the
interrupt is propagated inwards into the continuation $N$. On the other hand,
if the interrupt does not match the interrupt handler, it is simply propagated
past the interrupt handler into $N$. Finally, to simplify normal forms, we
propagate interrupts inside computations awaiting fulfilled promises as well.
As with the algebraicity rule, this lets the computation take a single
additional step after which the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
construct reaches the top and blocks the evaluation.

##### Awaiting a Promise To Be Fulfilled

In addition to the two rules for outwards propagation, the semantics of the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
construct includes a $\beta$-rule allowing the blocked computation $M$ to
resume executing as $M[V/x]$ when the
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$
in question is given a fulfilled promise $\langle V\rangle$.

##### Evaluation Contexts

The semantics allows reductions under _evaluation contexts_ $\mathcal{E}$.
Observe that as discussed earlier, the inclusion of interrupt handlers in the
evaluation contexts means that reductions involve potentially open terms.
Also, differently from the semantics of conventional operation calls [KLO13,
BP14], our evaluation contexts include outgoing signals. As such, the
_evaluation context rule_ allows the execution of a computation to proceed
even if a signal has not yet been propagated to its receiver, or when an
interrupt has not yet arrived. Importantly, the evaluation contexts do not
include
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}$,
so as to model its blocking behaviour. We write $\mathcal{E}[M]$ for the
operation of filling the hole $[~{}]$ in $\mathcal{E}$ with $M$.

##### Non-Confluence

It is worth noting that the asynchronous design means that the operational
semantics is _nondeterministic_. More interestingly, the semantics is also
_not confluent_.

For one source of non-confluence, let us consider two reduction sequences of a
same computation, where for better readability, we highlight the active redex
for each step:

$\begin{array}[]{r@{\,}
l}&\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M^{\prime}))\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\\!\leavevmode\hbox
to10.83pt{\vbox to8.54pt{\pgfpicture\makeatletter\hbox{\hskip
5.41606pt\lower-4.27023pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{1.41606pt}{4.27023pt}\pgfsys@lineto{-1.41606pt}{4.27023pt}\pgfsys@curveto{-3.62523pt}{4.27023pt}{-5.41606pt}{2.4794pt}{-5.41606pt}{0.27023pt}\pgfsys@lineto{-5.41606pt}{-0.27023pt}\pgfsys@curveto{-5.41606pt}{-2.4794pt}{-3.62523pt}{-4.27023pt}{-1.41606pt}{-4.27023pt}\pgfsys@lineto{1.41606pt}{-4.27023pt}\pgfsys@curveto{3.62523pt}{-4.27023pt}{5.41606pt}{-2.4794pt}{5.41606pt}{-0.27023pt}\pgfsys@lineto{5.41606pt}{0.27023pt}\pgfsys@curveto{5.41606pt}{2.4794pt}{3.62523pt}{4.27023pt}{1.41606pt}{4.27023pt}\pgfsys@closepath\pgfsys@moveto{-5.41606pt}{-4.27023pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.56248pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$N$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})\\\\[4.30554pt]
\leadsto&\leavevmode\hbox to368.65pt{\vbox
to14.3pt{\pgfpicture\makeatletter\hbox{\hskip 184.3263pt\lower-7.15158pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{180.3263pt}{7.15158pt}\pgfsys@lineto{-180.3263pt}{7.15158pt}\pgfsys@curveto{-182.53546pt}{7.15158pt}{-184.3263pt}{5.36075pt}{-184.3263pt}{3.15158pt}\pgfsys@lineto{-184.3263pt}{-3.15158pt}\pgfsys@curveto{-184.3263pt}{-5.36075pt}{-182.53546pt}{-7.15158pt}{-180.3263pt}{-7.15158pt}\pgfsys@lineto{180.3263pt}{-7.15158pt}\pgfsys@curveto{182.53546pt}{-7.15158pt}{184.3263pt}{-5.36075pt}{184.3263pt}{-3.15158pt}\pgfsys@lineto{184.3263pt}{3.15158pt}\pgfsys@curveto{184.3263pt}{5.36075pt}{182.53546pt}{7.15158pt}{180.3263pt}{7.15158pt}\pgfsys@closepath\pgfsys@moveto{-184.3263pt}{-7.15158pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-183.47272pt}{-3.798pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M^{\prime}))\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\\!\leavevmode\hbox
to12.37pt{\vbox to10.1pt{\pgfpicture\makeatletter\hbox{\hskip
6.18605pt\lower-5.048pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{2.18605pt}{5.048pt}\pgfsys@lineto{-2.18605pt}{5.048pt}\pgfsys@curveto{-4.39522pt}{5.048pt}{-6.18605pt}{3.25717pt}{-6.18605pt}{1.048pt}\pgfsys@lineto{-6.18605pt}{-1.048pt}\pgfsys@curveto{-6.18605pt}{-3.25717pt}{-4.39522pt}{-5.048pt}{-2.18605pt}{-5.048pt}\pgfsys@lineto{2.18605pt}{-5.048pt}\pgfsys@curveto{4.39522pt}{-5.048pt}{6.18605pt}{-3.25717pt}{6.18605pt}{-1.048pt}\pgfsys@lineto{6.18605pt}{1.048pt}\pgfsys@curveto{6.18605pt}{3.25717pt}{4.39522pt}{5.048pt}{2.18605pt}{5.048pt}\pgfsys@closepath\pgfsys@moveto{-6.18605pt}{-5.048pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-5.33247pt}{-4.19443pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$N^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leadsto&\leavevmode\hbox to341.57pt{\vbox
to16.8pt{\pgfpicture\makeatletter\hbox{\hskip 170.78462pt\lower-8.40158pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{166.78462pt}{8.40158pt}\pgfsys@lineto{-166.78462pt}{8.40158pt}\pgfsys@curveto{-168.99379pt}{8.40158pt}{-170.78462pt}{6.61075pt}{-170.78462pt}{4.40158pt}\pgfsys@lineto{-170.78462pt}{-4.40158pt}\pgfsys@curveto{-170.78462pt}{-6.61075pt}{-168.99379pt}{-8.40158pt}{-166.78462pt}{-8.40158pt}\pgfsys@lineto{166.78462pt}{-8.40158pt}\pgfsys@curveto{168.99379pt}{-8.40158pt}{170.78462pt}{-6.61075pt}{170.78462pt}{-4.40158pt}\pgfsys@lineto{170.78462pt}{4.40158pt}\pgfsys@curveto{170.78462pt}{6.61075pt}{168.99379pt}{8.40158pt}{166.78462pt}{8.40158pt}\pgfsys@closepath\pgfsys@moveto{-170.78462pt}{-8.40158pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-169.93105pt}{-5.048pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M[V/x])\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M^{\prime})\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\\!\leavevmode\hbox
to49.87pt{\vbox to12.6pt{\pgfpicture\makeatletter\hbox{\hskip
24.93604pt\lower-6.298pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{20.93604pt}{6.298pt}\pgfsys@lineto{-20.93604pt}{6.298pt}\pgfsys@curveto{-23.1452pt}{6.298pt}{-24.93604pt}{4.50717pt}{-24.93604pt}{2.298pt}\pgfsys@lineto{-24.93604pt}{-2.298pt}\pgfsys@curveto{-24.93604pt}{-4.50717pt}{-23.1452pt}{-6.298pt}{-20.93604pt}{-6.298pt}\pgfsys@lineto{20.93604pt}{-6.298pt}\pgfsys@curveto{23.1452pt}{-6.298pt}{24.93604pt}{-4.50717pt}{24.93604pt}{-2.298pt}\pgfsys@lineto{24.93604pt}{2.298pt}\pgfsys@curveto{24.93604pt}{4.50717pt}{23.1452pt}{6.298pt}{20.93604pt}{6.298pt}\pgfsys@closepath\pgfsys@moveto{-24.93604pt}{-6.298pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-24.08246pt}{-2.94443pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N^{\prime})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leadsto&\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M[V/x])\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M^{\prime}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N^{\prime}))\end{array}$

and

$\begin{array}[]{r@{\,} l}&\leavevmode\hbox to367.11pt{\vbox
to12.75pt{\pgfpicture\makeatletter\hbox{\hskip 183.5563pt\lower-6.37381pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{179.5563pt}{6.37381pt}\pgfsys@lineto{-179.5563pt}{6.37381pt}\pgfsys@curveto{-181.76547pt}{6.37381pt}{-183.5563pt}{4.58298pt}{-183.5563pt}{2.37381pt}\pgfsys@lineto{-183.5563pt}{-2.37381pt}\pgfsys@curveto{-183.5563pt}{-4.58298pt}{-181.76547pt}{-6.37381pt}{-179.5563pt}{-6.37381pt}\pgfsys@lineto{179.5563pt}{-6.37381pt}\pgfsys@curveto{181.76547pt}{-6.37381pt}{183.5563pt}{-4.58298pt}{183.5563pt}{-2.37381pt}\pgfsys@lineto{183.5563pt}{2.37381pt}\pgfsys@curveto{183.5563pt}{4.58298pt}{181.76547pt}{6.37381pt}{179.5563pt}{6.37381pt}\pgfsys@closepath\pgfsys@moveto{-183.5563pt}{-6.37381pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-182.70273pt}{-3.02023pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M^{\prime}))\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\\!\leavevmode\hbox
to10.83pt{\vbox to8.54pt{\pgfpicture\makeatletter\hbox{\hskip
5.41606pt\lower-4.27023pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{1.41606pt}{4.27023pt}\pgfsys@lineto{-1.41606pt}{4.27023pt}\pgfsys@curveto{-3.62523pt}{4.27023pt}{-5.41606pt}{2.4794pt}{-5.41606pt}{0.27023pt}\pgfsys@lineto{-5.41606pt}{-0.27023pt}\pgfsys@curveto{-5.41606pt}{-2.4794pt}{-3.62523pt}{-4.27023pt}{-1.41606pt}{-4.27023pt}\pgfsys@lineto{1.41606pt}{-4.27023pt}\pgfsys@curveto{3.62523pt}{-4.27023pt}{5.41606pt}{-2.4794pt}{5.41606pt}{-0.27023pt}\pgfsys@lineto{5.41606pt}{0.27023pt}\pgfsys@curveto{5.41606pt}{2.4794pt}{3.62523pt}{4.27023pt}{1.41606pt}{4.27023pt}\pgfsys@closepath\pgfsys@moveto{-5.41606pt}{-4.27023pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-4.56248pt}{-3.41666pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$N$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}})$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leadsto&\leavevmode\hbox to340.03pt{\vbox
to15.91pt{\pgfpicture\makeatletter\hbox{\hskip
170.01462pt\lower-7.95715pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{0.83,0.83,0.83}\pgfsys@color@rgb@fill{0.83}{0.83}{0.83}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{166.01462pt}{7.95715pt}\pgfsys@lineto{-166.01462pt}{7.95715pt}\pgfsys@curveto{-168.22379pt}{7.95715pt}{-170.01462pt}{6.16632pt}{-170.01462pt}{3.95715pt}\pgfsys@lineto{-170.01462pt}{-3.95715pt}\pgfsys@curveto{-170.01462pt}{-6.16632pt}{-168.22379pt}{-7.95715pt}{-166.01462pt}{-7.95715pt}\pgfsys@lineto{166.01462pt}{-7.95715pt}\pgfsys@curveto{168.22379pt}{-7.95715pt}{170.01462pt}{-6.16632pt}{170.01462pt}{-3.95715pt}\pgfsys@lineto{170.01462pt}{3.95715pt}\pgfsys@curveto{170.01462pt}{6.16632pt}{168.22379pt}{7.95715pt}{166.01462pt}{7.95715pt}\pgfsys@closepath\pgfsys@moveto{-170.01462pt}{-7.95715pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-169.16104pt}{-4.60358pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M[V/x])\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;M^{\prime})\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\\!\leavevmode\hbox
to48.33pt{\vbox to11.71pt{\pgfpicture\makeatletter\hbox{\hskip
24.16603pt\lower-5.85358pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}}{}{}{}{}{}
{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor[named]{pgffillcolor}{rgb}{1,1,1}\pgfsys@color@gray@fill{1}\pgfsys@invoke{
}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}{{}{}{{}}}{{}{}{{}}}{}{}\pgfsys@moveto{20.16603pt}{5.85358pt}\pgfsys@lineto{-20.16603pt}{5.85358pt}\pgfsys@curveto{-22.3752pt}{5.85358pt}{-24.16603pt}{4.06274pt}{-24.16603pt}{1.85358pt}\pgfsys@lineto{-24.16603pt}{-1.85358pt}\pgfsys@curveto{-24.16603pt}{-4.06274pt}{-22.3752pt}{-5.85358pt}{-20.16603pt}{-5.85358pt}\pgfsys@lineto{20.16603pt}{-5.85358pt}\pgfsys@curveto{22.3752pt}{-5.85358pt}{24.16603pt}{-4.06274pt}{24.16603pt}{-1.85358pt}\pgfsys@lineto{24.16603pt}{1.85358pt}\pgfsys@curveto{24.16603pt}{4.06274pt}{22.3752pt}{5.85358pt}{20.16603pt}{5.85358pt}\pgfsys@closepath\pgfsys@moveto{-24.16603pt}{-5.85358pt}\pgfsys@fill\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-23.31245pt}{-2.5pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys<EMAIL_ADDRESS>\leadsto&\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op^{\prime}}\;y\mapsto
M[V/x])\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}await}\;q\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}until}\;\langle
z\rangle\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;(\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M^{\prime}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N))\end{array}$

Here, both final computations are _temporarily_ blocked until an incoming
interrupt $\mathsf{op^{\prime}}$ is propagated to them and the variable $q$
gets bound to a fulfilled promise. Until this happens, it is not possible for
the blocked continuation $N$ to reduce to $N^{\prime}$ in the latter final
computation.

Another, distinct source of non-confluence concerns the commutativity of
outgoing signals with enveloping interrupt handlers. For instance, the
following composite computation

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(W^{\prime},M))\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime\prime}}\,(W^{\prime\prime},N)})$

can nondeterministically reduce to either

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(W^{\prime},\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime\prime}}\,(W^{\prime\prime},{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)}))$

if we first propagate the interrupt $\mathsf{op}$ inwards, or to

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime\prime}}\,(W^{\prime\prime},\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(W^{\prime},{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}let}\;p=M\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,N)}))$

if we first propagate the signal $\mathsf{op}^{\prime\prime}$ outwards. As a
result, in the resulting two computations, the signals $\mathsf{op}^{\prime}$
and $\mathsf{op}^{\prime\prime}$ get issued, and received by other processes,
in a different order.

###  3.3. Type-and-Effect System

We equip $\lambda_{\text{\ae}}$ with a type system in the tradition of type-
and-effect systems for algebraic effects and effect handlers [BP14, KLO13], by
extending the simple type system of FGCBV with annotations about programs’
possible effects (such as issued signals and installed interrupt handlers) in
function and computation types.

####  3.3.1. Types

We define types in Figure 3, separated into ground, value, and computation
types.

$\displaystyle\text{Ground type $A$, $B$}\mathrel{\;{:}{:}{=}\ }$
$\displaystyle\mathsf{b}\mathrel{\,\;\big{|}\ \
\\!}\mathsf{1}\mathrel{\,\;\big{|}\ \ \\!}\mathsf{0}\mathrel{\,\;\big{|}\ \
\\!}A\times B\mathrel{\,\;\big{|}\ \ \\!}A+B$ Signal or interrupt signature:
$\displaystyle\mathsf{op}:A_{\mathsf{op}}$ Outgoing signal annotations:
$\displaystyle o\in O$ Interrupt handler annotations: $\displaystyle\iota\in
I$ $\displaystyle\text{Value type $X$, $Y$}\mathrel{\;{:}{:}{=}\ }$
$\displaystyle A\mathrel{\,\;\big{|}\ \ \\!}X\times Y\mathrel{\,\;\big{|}\ \
\\!}X+Y\mathrel{\,\;\big{|}\ \ \\!}X\to Y\and(o,\iota)\mathrel{\,\;\big{|}\ \
\\!}\langle X\rangle$ Computation type: $\displaystyle X\and(o,\iota)$
$\displaystyle\text{Typing context $\Gamma$}\mathrel{\;{:}{:}{=}\ }$
$\displaystyle\cdot\mathrel{\,\;\big{|}\ \ \\!}\Gamma,x\mathinner{:}X$

Figure 3. Value and Computation Types.

As noted in Section 3.1, $\lambda_{\text{\ae}}$ is parameterised over a set
$\Sigma$ of signal and interrupt _names_. To each such name
$\mathsf{op}\in\Sigma$, we assign a _signature_ $\mathsf{op}:A_{\mathsf{op}}$
that specifies the payload type $A_{\mathsf{op}}$ of the corresponding signal
or interrupt. Crucially, in order to be able to later prove that
$\lambda_{\text{\ae}}$ is type safe, we must put restrictions on these
signatures. In particular, the reduction rule

$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(V,N)\leadsto\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\uparrow}\,\mathsf{op^{\prime}}\,(V,\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}promise}\;(\mathsf{op}\;x\mapsto
M)\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}as}\;p\;\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}in}\;N)$

that propagates signals out of interrupt handlers can break type preservation
if the payload $V$ depends on the promise variable $p$. In Section 5.3, we
discuss a more flexible type system that uses modal types to classify values
that may cross interrupt handler or process boundaries, but for the sake of
exposition, we use here the more limited approach from our previous work
[AP21], and restrict payload types to _ground types_ $A,B,\ldots$, which
include base, unit, empty, product, and sum types, but importantly exclude
promise and function types.

_Value types_ $X,Y,\ldots$ extend ground types with function and promise
types. The _function type_ $X\to Y\and(o,\iota)$ classifies functions that
take $X$-typed arguments to computations classified by the _computation type_
$Y\and(o,\iota)$, i.e., ones that return $Y$-typed values, while possibly
issuing signals specified by $o$ and handling interrupts specified by $\iota$.
The _effect annotations_ $o$ and $\iota$ are drawn from sets $O$ and $I$ whose
definitions we discuss in Section 3.3.2. The $\lambda_{\text{\ae}}$-specific
_promise type_ $\langle X\rangle$ classifies promises that can be fulfilled by
supplying a value of type $X$.

####  3.3.2. Effect Annotations

We now explain how we define the sets $O$ and $I$ from which we draw the
effect annotations we use for specifying functions and computations.
Traditionally, effect systems for algebraic effects simply use (flat) sets of
operation names for effect annotations [BP14, KLO13]. In
$\lambda_{\text{\ae}}$, however, we need to be more careful, because
triggering an interrupt handler executes a computation that can issue
potentially different signals and handle different interrupts from the main
program, and we would like to capture this in types.

##### Signal Annotations

First, as outgoing signals do not carry any computational data, we follow the
tradition of type-and-effect systems for algebraic effects, and define $O$ to
be the _power set_ $\mathcal{P}(\Sigma)$. As such, each $o\in O$ is a subset
of the signature $\Sigma$, specifying which signals a computation might issue
(this is an over-approximation of the actually issued signals).

##### Interrupt Handler Annotations

As observed above, for specifying installed interrupt handlers, we cannot use
(flat) sets of interrupt names as the effect annotations $\iota\in I$ if we
want to track the nested (and sometimes recursive) effectful structure of
interrupt handlers.

Instead, intuitively each $\iota\in I$ is a _possibly infinite_ nesting of
partial mappings of pairs of $O$\- and $I$-annotations to names in
$\Sigma$—these pairs of annotations classify the possible effects of the
corresponding interrupt handler code. We use the record notation

$\iota=\\{\mathsf{op}_{1}\mapsto(o_{1},\iota_{1}),\ldots,\mathsf{op}_{n}\mapsto(o_{n},\iota_{n})\\}$

to mean that $\iota$ maps $\mathsf{op}_{1},\ldots,\mathsf{op}_{n}$ to the
annotations $(o_{1},\iota_{1}),\ldots,(o_{n},\iota_{n})$, while any other
names in $\Sigma$ are unannotated, corresponding to no interrupt handlers
being installed for these other names. We write
$\iota\,(\mathsf{op}_{i})=(o_{i},\iota_{i})$ to mean that the annotation
$\iota$ maps $\mathsf{op}_{i}$ to $(o_{i},\iota_{i})$.

Formally, we define $I$ as the _greatest fixed point_ of a set functor $\Phi$,
given by

$\Phi(X)\mathrel{\overset{\text{\tiny def}}{=}}\Sigma\Rightarrow(O\times
X)_{\bot}$

where $\Rightarrow$ is exponentiation, $\times$ is Cartesian product, and
$(-)_{\bot}$ is the lifting operation, which we use to represent unannotated
names, and which is defined using the disjoint union as
$(-)\mathbin{\mathchoice{\ooalign{$\displaystyle\cup$\cr$\displaystyle\cdot$}}{\ooalign{$\textstyle\cup$\cr$\textstyle\cdot$}}{\ooalign{$\scriptstyle\cup$\cr$\scriptstyle\cdot$}}{\ooalign{$\scriptscriptstyle\cup$\cr$\scriptscriptstyle\cdot$}}}\\{\bot\\}$.
Formally speaking, $I$ is given by an isomorphism $I\cong\Phi(I)$, but for
presentation purposes we leave it implicit and work as if we had a strict
equality $I=\Phi(I)$.

##### Subtyping and Recursive Effect Annotations

Both $O$ and $I$ come equipped with natural _partial orders_ : for $O$,
$\sqsubseteq_{O}$ is given simply by subset inclusion; and for $I$, the
pointwise order $\sqsubseteq_{I}$ is characterised as follows:

$\begin{array}[]{l c
l}\iota\sqsubseteq_{I}\iota^{\prime}&\text{iff}&\forall\,(\mathsf{op}\in\Sigma)\,(o^{\prime\prime}\in
O)\,(\iota^{\prime\prime}\in
I).\,\iota\,(\mathsf{op})=({o^{\prime\prime}},{\iota^{\prime\prime}})\implies\\\\[2.15277pt]
&&\exists\,(o^{\prime\prime\prime}\in O)\,(\iota^{\prime\prime\prime}\in
I).\,\iota^{\prime}\,(\mathsf{op})=({o^{\prime\prime\prime}},{\iota^{\prime\prime\prime}})\wedge
o^{\prime\prime}\sqsubseteq_{O}o^{\prime\prime\prime}\wedge\iota^{\prime\prime}\sqsubseteq_{I}\iota^{\prime\prime\prime}\end{array}$

We also use the _product order_ $\sqsubseteq_{O\times I}$, defined as
$(o,\iota)\sqsubseteq_{O\times
I}(o^{\prime},\iota^{\prime})\mathrel{\overset{\text{\tiny
def}}{=}}o\sqsubseteq_{O}o^{\prime}\wedge\iota\sqsubseteq_{I}\iota^{\prime}$.
In particular, we use $\sqsubseteq_{O\times I}$ to define the subtyping
relation for $\lambda_{\text{\ae}}$’s computation types.

Furthermore, both $O$ and $I$ carry a _join-semilattice_ structure, where
$o\sqcup o^{\prime}\in O$ is given simply by the union of sets, while
$\iota\sqcup\iota^{\prime}\in I$ is given pointwise as follows:

$(\iota\sqcup\iota^{\prime})(\mathsf{op})~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\begin{cases}(o^{\prime\prime}\sqcup
o^{\prime\prime\prime},\iota^{\prime\prime}\sqcup\iota^{\prime\prime\prime})&\mbox{if
}\iota\,(\mathsf{op})=(o^{\prime\prime},\iota^{\prime\prime})\wedge\iota^{\prime}\,(\mathsf{op})=(o^{\prime\prime\prime},\iota^{\prime\prime\prime})\\\
(o^{\prime\prime},\iota^{\prime\prime})&\mbox{if
}\iota\,(\mathsf{op})=(o^{\prime\prime},\iota^{\prime\prime})\wedge\iota^{\prime}\,(\mathsf{op})=\bot\\\
(o^{\prime\prime\prime},\iota^{\prime\prime\prime})&\mbox{if
}\iota\,(\mathsf{op})=\bot\wedge\iota^{\prime}\,(\mathsf{op})=(o^{\prime\prime\prime},\iota^{\prime\prime\prime})\\\
\bot&\mbox{if
}\iota\,(\mathsf{op})=\bot\wedge\iota^{\prime}\,(\mathsf{op})=\bot\\\
\end{cases}$

Importantly, the partial orders $(O,\sqsubseteq_{O})$ and
$(I,\sqsubseteq_{I})$ are both _$\omega$ -complete_ and _pointed_ , i.e., they
form _pointed $\omega$-cpos_, meaning that they have least upper bounds of all
increasing $\omega$-chains, and least elements (given by the empty set
$\emptyset$ and the constant $\bot$-valued mapping, respectively). As a
consequence, and as is well-known, _least fixed points_ of continuous
(endo)maps on them are then guaranteed to exist [AC98, GHK+03]. For
$\lambda_{\text{\ae}}$, we are particularly interested in the least fixed
points of continuous maps $f:I\to I$, so as to specify and typecheck code
examples involving reinstallable interrupt handlers, as we illustrate in
Section 5.1.

We also note that if we were only interested in the type safety of
$\lambda_{\text{\ae}}$, and not in typechecking reinstallable interrupt
handler examples, then we would not need $(I,\sqsubseteq_{I})$ to be _$\omega$
-complete_, and could have instead chosen $I$ to be the _least fixed point_ of
the set functor $\Phi$ defined earlier, which is what we do for simplicity in
our Agda formalisation. In this case, each interrupt handler annotation
$\iota\in I$ would be a _finite nesting of partial mappings_.

Finally, we envisage that any future full-fledged high-level language based on
$\lambda_{\text{\ae}}$ would allow users to define their (recursive) effect
annotations in a small domain-specific language, providing a syntactic
counterpart to the domain-theoretic development we use in this paper.

##### Interrupt Actions

We mimic the act of triggering an interrupt handler for some interrupt
$\mathsf{op}$ on an effect annotation $(o,\iota)$ through an _action_ defined
as follows:

${\mathsf{op}}\,{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}}\,(o,\iota)~{}\mathrel{\overset{\text{\tiny
def}}{=}}~{}\begin{cases}\left(o\sqcup
o^{\prime},\iota[\mathsf{op}\mapsto\bot]\sqcup\iota^{\prime}\right)&\mbox{if
}\iota\,(\mathsf{op})=(o^{\prime},\iota^{\prime})\\\
(o,\iota)&\mbox{otherwise}\end{cases}$

If $(o,\iota)$ lists any interrupt handlers installed for $\mathsf{op}$, then
$\iota\,(\mathsf{op})=(o^{\prime},\iota^{\prime})$, where
$(o^{\prime},\iota^{\prime})$ specifies the effects of said handler code. Now,
when the inward propagating interrupt reaches those interrupt handlers, it
triggers the execution of the corresponding handler code, and thus the entire
interrupted computation can also issue signals in $o^{\prime}$ and handle
interrupts in $\iota^{\prime}$.

The notation $\iota[\mathsf{op}\mapsto\bot]$ sets $\iota$ to $\bot$ at
$\mathsf{op}$, and leaves it unchanged elsewhere. Mapping $\mathsf{op}$ to
$\bot$ captures that the interrupt triggers all the corresponding interrupt
handlers in $M$.

####  3.3.3. Typing Rules

We characterise _well-typed values_ using the judgement $\Gamma\vdash V:X$ and
_well-typed computations_ using the judgement $\Gamma\vdash M:X\and(o,\iota)$.
In both judgements, $\Gamma$ is a _typing context_. The rules defining these
judgements are respectively given in Figure 4 and 5.

*[Lab=TyVal-Var] Γ, x :X, Γ’ ⊢x : X *[Lab=TyVal-Unit] Γ⊢(): 1 *[Lab=TyVal-Pair] Γ⊢V : X
Γ⊢W : Y Γ⊢( V , W ) : X ×Y *[Lab=TyVal-Promise] Γ⊢V : X Γ⊢⟨V ⟩ : ⟨X ⟩
*[Lab=TyVal-Inl] Γ⊢V : X Γ⊢inl_Y V : X + Y *[Lab=TyVal-Inr] Γ⊢W : Y Γ⊢inr_X W : X + Y *[Lab=TyVal-Fun] Γ, x :X ⊢M : Y and (o,ι) Γ⊢fun (x : X) ↦M : X →Y and (o,ι)

Figure 4. Value Typing Rules.

*[Lab=TyComp-Return] Γ⊢V : X Γ⊢return_ V : X and (o,ι) *[Lab=TyComp-Let] Γ⊢M : X and (o,ι)
Γ, x :X ⊢N : Y and (o,ι) Γ⊢let x = M in N : Y and (o,ι)
*[Lab=TyComp-Apply] Γ⊢V : X →Y and (o,ι)
Γ⊢W : X Γ⊢V W : Y and (o,ι) *[Lab=TyComp-MatchPair] Γ⊢V : X ×Y
Γ, x :X, y :Y ⊢M : Z and (o,ι) Γ⊢match V with {( x , y ) ↦M}_ : Z and (o,ι)
*[Lab=TyComp-MatchEmpty] Γ⊢V : 0 Γ⊢match V with {}_Z and (o,ι) : Z and (o,ι) *[Lab=TyComp-MatchSum] Γ⊢V : X + Y

Γ, x :X ⊢M : Z and (o,ι)
Γ, y :Y ⊢N : Z and (o,ι)
Γ⊢match V with {inl_ x ↦M, inr_ y ↦N}_ : Z and (o,ι)
*[Lab=TyComp-Signal] op∈o
Γ⊢V : A_op
Γ⊢M : X and (o,ι) Γ⊢↑ op (V, M) : X and (o,ι) *[Lab=TyComp-Interrupt] Γ⊢V :
A_op
Γ⊢M : X and (o,ι) Γ⊢↓ op (V, M) : X and op ↓ (o,ι)
*[Lab=TyComp-Promise] (o’ , ι’) = ι (op)
Γ, x :A_op⊢M : ⟨X ⟩ and (o’,ι’)
Γ, p :⟨X ⟩ ⊢N : Y and (o,ι) Γ⊢promise (op x ↦M) as p in N : Y and (o,ι)
*[Lab=TyComp-Await] Γ⊢V : ⟨X ⟩
Γ, x :X ⊢M : Y and (o,ι) Γ⊢await V until ⟨x ⟩ in M : Y and (o,ι) *[Lab=TyComp-
Subsume] Γ⊢M : X and (o, ι)
(o,ι) ⊑_O ×I (o’,ι’) Γ⊢M : X and (o’, ι’)

Figure 5. Computation Typing Rules.

##### Values

The rules for values are mostly standard. The only
$\lambda_{\text{\ae}}$-specific rule is TyVal-Promise, which states that in
order to fulfil a _promise_ of type $\langle X\rangle$, one has to supply a
value of type $X$. In the rule TyVal-Var, we emphasise the position of the
variable in the context, as it will become important once we extend the
calculus with modal types in Section 5.3.

##### Computations

Analogously to values, the typing rules are standard for computation terms
that $\lambda_{\text{\ae}}$ inherits from FGCBV, with the
$\lambda_{\text{\ae}}$-rules additionally tracking effect information.

The first $\lambda_{\text{\ae}}$-specific typing rule TyComp-Signal states
that in order to issue a signal $\mathsf{op}$ in a computation that has type
$X\and(o,\iota)$, we must have $\mathsf{op}\in o$ and the type of the payload
value has to match $\mathsf{op}$’s signature $\mathsf{op}:A_{\mathsf{op}}$.

The rule TyComp-Interrupt is used to type incoming interrupts. In particular,
when the outside world propagates an interrupt $\mathsf{op}$ to a computation
$M$ of type $X\and(o,\iota)$, the resulting computation
$\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}\,\mathsf{op}\,(V,M)$
gets assigned the type
$X\and{\mathsf{op}}\,{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}}\,(o,\iota)$,
where the action
${\mathsf{op}}\,{\mathsf{\color[rgb]{0.0,0.0,0.5}\definecolor[named]{pgfstrokecolor}{rgb}{0.0,0.0,0.5}\downarrow}}\,(o,\iota)$
of the interrupt $\mathsf{op}$ on the annotation $(o,\iota)$ is given as
discussed in Section 3.3.2.

The rule TyComp-Promise states that the interrupt handler code $M$ has to
return a fulfilled promise of type $\langle X\rangle$, for some type $X$,
while possibly issuing signals $o^{\prime}$ and handling interrupts
$\iota^{\prime}$, both of which are determined by the effect annotation
$\iota$ of the entire computation, as
$(o^{\prime},\iota^{\prime})=\iota\,(\mathsf{op})$. The variable $p$ bound in
the continuation, which sub-computations can block on to await $\mathsf{op}$
to arrive and be handled, also gets assigned the promise type $\langle
X\rangle$.

It is worth noting that we could have had $M$ simply return values of type
$X$, but at the cost of not being able to implement some of the more