# Lang-n-Send: Processes That Send Languages

Matteo Cimini University of Massachusetts Lowell
Lowell, MA, USA<EMAIL_ADDRESS>
###### Abstract

We present Lang-n-Send, a $\pi$-calculus that is equipped with language
definitions. Processes can define languages in operational semantics, and use
them to execute programs. Furthermore, processes can send and receive pieces
of operational semantics through channels.

We present a reduction semantics for Lang-n-Send, and we offer examples that
demonstrate some of the scenarios that Lang-n-Send captures.

##  1 Introduction

In the last decades, we have seen significant advances in language semantics
tools that make it possible for programmers to quickly define and deploy their
own programming languages and domain-specific languages, and use them in their
programming solutions [7].

It is not too far in the future that it would just be the common practice for
programmers to upload, in servers like Amazon AWS, code that does not belong
to a programming language that has been fixed beforehand, but rather belongs
to a language that has been created on the fly. Programmers would upload both
the program and the language in which the program must be evaluated. Reuse is
fundamental in this scenario. Libraries of programming languages constructs,
as envisioned by Peter Mosses’ Component-Based Semantics [15], for example,
can become the norm. Servers can provide pieces of languages to clients, which
can use them to complete their own language and, in turn, send the language so
built to (computing) servers to execute programs.

Current literature does not offer a foundation that directly formalizes this
and similar scenarios. In this paper, we present our work towards such a
formal foundation.

We present Lang-n-Send, a $\pi$-calculus that is equipped with language
definitions. Processes can define languages in operational semantics, add
pieces of operational semantics together, and use them to execute programs.
Processes can also send and receive pieces of languages through channels.
After executing programs, Lang-n-Send processes can also send the trace of
executions to other processes, which in turn can analyze these traces.

We present a reduction semantics for Lang-n-Send, and we provide some selected
examples that demonstrate the scenarios that Lang-n-Send captures. We have
specifically chosen examples that involve the communication of languages among
processes. We show the following examples:

  * •

A client that, when entering a sensitive region of code, asks a server to
provide the semantics of an interrupt operator, adds it to its language, and
only then executes the code.

  * •

A client that defines a language with an interrupt operator, but lets a server
decide the semantics of the interruption (whether interrupt or disrupt
semantics) by receiving, from the server, the rest of the rules that complete
the semantics of the operator.

  * •

A client that lets a server decide whether its language is synchronous or
asynchronous by receiving the semantics of the output operator from the
server.

We believe that Lang-n-Send represents a first step towards a firm foundation
for this type of programming. The next section presents the syntax that Lang-
n-Send uses to define languages. Section 3 presents the syntax of Lang-n-Send
processes. Section 4 presents a reduction semantics. Section 5 provides
examples. Section 6 discusses related work, and Section 7 concludes the paper.

##  2 Syntax for Language Definitions

The syntax of Lang-n-Send consists of two parts: the syntax for creating
languages, and a $\pi$-calculus with language definitions. Language
definitions can be created in operational semantics. The syntax that we adopt
is inspired by [6], and is the following, where
$\textit{cname}\in\textsc{CatName}$, $X\in\textsc{Meta-Var}$,
$\textit{opname}\in\textsc{OpName}$, and $\textit{pn}\in\textsc{PredName}$.

$\begin{array}[]{l@{\;\;}lcl}\text{\sf Language}&\mathcal{L}&::=&(G,I)\\\
\text{\sf Grammar}&G&::=&s_{\\_}1\;\cdots\;s_{\\_}n\\\ \text{\sf{Grammar
Rule}}&s&::=&\textit{cname}\;X::=t_{\\_}1\;\mid\cdots\;\mid\;t_{\\_}n\\\
\text{\sf Inference System}&I&::=&r_{\\_}1\;\cdots\;r_{\\_}n\\\ \text{\sf
Rule}&r&::=&\inference{f_{\\_}1\;\cdots\;f_{\\_}n}{f}\\\ \text{\sf
Formula}&f&::=&(\textit{pn}\;t_{\\_}1\cdots\;t_{\\_}n)\\\ \text{\sf
Term}&t&::=&X\mid(\textit{opname}\;t_{\\_}1\cdots\;t_{\\_}n)\end{array}$

CatName is a set of grammar category names such as Process, and Action. Meta-
Var is a set of meta-variables. OpName is a set of constructor names such as
par (for the parallel operator $\mid$), and choice (for the choice operator
$+$). PredName is a set of predicate names such as step (for reduction rules).
As names do not need to be strings, we shall use symbols for constructor and
predicate names.

A language has a grammar and an inference rule system. A grammar has multiple
grammar rules, each of which defines a category name, and its meta-variable,
by providing a series of grammar productions, which are terms. Terms are in
abstract syntax tree style, that is, they have a top level constructor applied
to a list of terms. We can demonstrate Lang-n-Send with languages that do not
use binders. Therefore, we do not include syntax for binding, though it could
be added.

An inference rule system has multiple rules, each of which has a series of
formulae as premises, and a formula as conclusion. Formulae, too, are in
abstract syntax tree style. Given a language definition, Lang-n-Send needs to
invoke its evaluator to execute programs. As we need a way to locate such
evaluator, we fix the following convention: The labeled transition relation is
always $\longrightarrow$, and its first argument is always the label of the
transition, which is a term. (If reductions do not have labels, they would
still use the first argument with a term that is never used).

To make an example, let us consider Basic Process Algebra (BPA [4]) in its
finite fragment (no recursion, nor definitions). BPA is formed with actions,
the choice operator, and sequential composition. Below are the rules of BPA,
where $a$ ranges over actions. Besides transitions of the form
$P\stackrel{{\scriptstyle a}}{{\longrightarrow}}P^{\prime}$, BPA makes use of
a predicate $P\longrightarrow^{a}\checkmark$ that says that $P$ takes action
$a$ and successfully terminates.

$\displaystyle
a\longrightarrow^{a}\checkmark\quad\inference{P_{\\_}1\longrightarrow^{a}\checkmark}{P_{\\_}1+P_{\\_}2\longrightarrow^{a}\checkmark}\quad\inference{P_{\\_}2\longrightarrow^{a}\checkmark}{P_{\\_}1+P_{\\_}2\longrightarrow^{a}\checkmark}$
$\displaystyle\inference{P_{\\_}1\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}1^{\prime}}{P_{\\_}1+P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}1^{\prime}}\quad\inference{P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}2^{\prime}}{P_{\\_}1+P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}2^{\prime}}\quad\inference{P_{\\_}1\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}1^{\prime}}{P_{\\_}1\cdot
P_{\\_}2\stackrel{{\scriptstyle a}}{{\longrightarrow}}P_{\\_}1^{\prime}\cdot
P_{\\_}2}\quad\inference{P_{\\_}1\longrightarrow^{a}\checkmark}{P_{\\_}1\cdot
P_{\\_}2\stackrel{{\scriptstyle a}}{{\longrightarrow}}P_{\\_}2}$

Lang-n-Send accommodates BPA as follows. The transition
$P\stackrel{{\scriptstyle a}}{{\longrightarrow}}P^{\prime}$ is encoded as
$(\longrightarrow\;a\;P\;P^{\prime})$. We represent the formula
$P\longrightarrow^{a}\checkmark$ with $(\textit{checkMark}\;(a)\;P)$. Below,
act is the operator for actions, and seq is the sequential operator. We give
this language the name bpa.

$\displaystyle\textit{bpa}\triangleq($ $\displaystyle
Action\;A::=(\textit{a})\mid(\textit{b})\mid(\textit{c})\quad\qquad\textit{(*
We assume that the set of actions is $\\{a,b,c\\}$ *)}$ $\displaystyle
Process\;P::=(\textit{act}\;A)\mid(\textit{+}\;P\;P)\mid(\textit{seq}\;P\;P),$
$\displaystyle(\textit{checkMark}\;A\;(\textit{act}\;A))\quad\inference{(\textit{checkMark}\;A\;P_{\\_}1)}{(\textit{checkMark}\;A\;(+\;P_{\\_}1\;P_{\\_}2))}\quad\inference{(\textit{checkMark}\;A\;P_{\\_}2)}{(\textit{checkMark}\;A\;(+\;P_{\\_}1\;P_{\\_}2))}$
$\displaystyle\inference{{(\longrightarrow\;A\;P_{\\_}1\;P_{\\_}1^{\prime})}}{(\longrightarrow\;A\;(+\;P_{\\_}1\;P_{\\_}2)\;P_{\\_}1^{\prime})}\quad\inference{{(\longrightarrow\;A\;P_{\\_}2\;P_{\\_}2^{\prime})}}{(\longrightarrow\;A\;(+\;P_{\\_}1\;P_{\\_}2)\;P_{\\_}2^{\prime})}$
$\displaystyle\inference{{(\longrightarrow\;A\;P_{\\_}1\;P_{\\_}1^{\prime})}}{(\longrightarrow\;A\;(\textit{seq}\;P_{\\_}1\;P_{\\_}2)\;(\textit{seq}\;P_{\\_}1^{\prime}\;P_{\\_}2))}\quad\inference{(\textit{checkMark}\;A\;P_{\\_}1)}{(\longrightarrow\;A\;(\textit{seq}\;P_{\\_}1\;P_{\\_}2)\;P_{\\_}2)}~{}~{})$

##  3 Syntax for Processes

The syntax of Lang-n-Send processes $P$, $Q$, $R$, and so on, is defined as
follows.

$\begin{array}[]{l@{\;\;}lcl}\text{\sf Trace}&\mathfrak{T}&::=&\textit{tr}\mid
t\;\cdots\;t\\\ \text{\sf Language
Builder}&\ell&::=&l\mid\mathcal{L}\mid\ell\;\mathtt{union}\;\ell\\\ \text{\sf
Processes}&P&::=&\mathbf{0}\mid~{}x(y).P~{}\mid~{}\overline{x}\langle
y\rangle.P\mid~{}P\mid P~{}\mid~{}P+P{}\\\ &&&\mid~{}(\nu x).P~{}\mid~{}!P\\\
\textit{(}using~{}languages)&&&\mid\texttt{(}\ell,\mathfrak{T}\texttt{)}\texttt{>}_{x}\;t\\\
\textit{(}analyzing~{}executions)&&&\mid\mathtt{isInTrace}(t,\mathfrak{T})\Rightarrow
P~{};~{}P\\\
\textit{(}communicating~{}languages)&&&\mid~{}x(l).P~{}\mid~{}\overline{x}\langle\ell\rangle.P\\\
\textit{(}communicating~{}traces)&&&\mid~{}x(\textit{tr}).P~{}\mid~{}\overline{x}\langle\mathfrak{T}\rangle.P\\\
\end{array}$

Lang-n-Send contains the elements of the $\pi$-calculus [13, 14]. Channels are
$x$, $y$, $z$, and so on. We assume a set lang-var of variables $l$ for
languages, and a set trace-var of variables tr for traces. These sets are
distinct from each other, and from the set of channels.

_Language builder expressions_ $\ell$ build a language $\mathcal{L}$, i.e.,
they ultimately evaluate to a language $\mathcal{L}$. This category can be
extended with sophisticated language manipulations. We keep our syntax with
the minimal set of operations that are enough to demonstrate our approach.
Thus, we have included only a union operation for languages. $\mathtt{union}$
adds new grammar productions and inference rules to a language. For example,
$\textit{bpa}\;\mathtt{union}\;(Process\;P::=(\textit{loopOnNil}\;P))~{}(\longrightarrow\;A\;(\textit{loopOnNil}\;(\textit{nil}))\;(\textit{loopOnNil}\;(\textit{nil})))\,)$
returns the language with the same grammar productions for Action, and with
the additional production $(\textit{loopOnNil}\;P)$ for $P$. Also, the rule
above for loopOnNil is added to the rules of bpa.

Lang-n-Send extends the processes of the $\pi$-calculus with the following
constructors. A process
$\texttt{(}\ell,\mathfrak{T}\texttt{)}\texttt{>}_{x}\;{t}$ is a _program
execution_. This process executes the program $t$ according to the operational
semantics defined in the language $\ell$. In particular, we query the language
for reductions that are provable with $\longrightarrow$. We also keep track of
the trace of executions. Traces are sequences of labels. As we use terms to
represent labels, our traces $\mathfrak{T}$ are sequences of terms. We assume
that a program execution starts with an empty sequence of labels, which we
denote with $[]$ to avoid a confusing empty space in our examples. A reduction
step of $t$ carries a label, and we append it to $\mathfrak{T}$. Then,
$\mathfrak{T}$ contains all the labels of all the steps of $t$, that is,
$\mathfrak{T}$ is a trace of the execution of $t$. When the execution of $t$
terminates, the trace is sent over the channel $x$.

To make an example:

$\texttt{(}\textit{bpa},[]\texttt{)}\texttt{>}_{x}\;(\textit{seq}\;(\textit{act}\;(a))\;(\textit{seq}\;(\textit{act}\;(b))\;(\textit{act}\;(c))))$
reduces to

$\texttt{(}\textit{bpa},(a)\texttt{)}\texttt{>}_{x}\;(\textit{seq}\;(\textit{act}\;(b))\;(\textit{act}\;(c)))$
which reduces to

$\texttt{(}\textit{bpa},(a)~{}(b)\texttt{)}\texttt{>}_{x}\;(\textit{act}\;(c))$
which reduces to $\overline{x}\langle(a)~{}(b)\rangle.\mathbf{0}$.

Notice that, in BPA, this last $c$ does not take a transition, but
$c\longrightarrow^{c}\checkmark$ holds. We could account for this with a
straightforward modification of BPA that performs the last action as a labeled
transition, but we prefer to use its original formulation.

A process $\mathtt{isInTrace}(t,\mathfrak{T})\Rightarrow P~{};~{}Q$ checks
whether the label $t$ is one of the labels in the trace $\mathfrak{T}$. In
that case, this process behaves as $P$, otherwise it behaves as $Q$.

A process $x(l).P$ is a _language input prefix_. This process receives a
language on the channel $x$, binds it to $l$, and continues as $P$. A process
$\overline{x}\langle\ell\rangle.P$ is a _language output prefix_. This process
evaluates $\ell$ to a language $\mathcal{L}$, sends it over the channel $x$,
and continues as $P$. Similarly, a process $x(\textit{tr}).P$ is a _trace
input prefix_ and receives traces. A process
$\overline{x}\langle\mathfrak{T}\rangle.P$ is a _trace output prefix_ and
sends traces.

##  4 A Reduction Semantics for Lang-n-Send

Figure 4 shows the reduction semantics of Lang-n-Send. Structural congruence
$\equiv$ is standard. The reduction relation for the processes of Lang-n-Send
is $\longrightarrow$. This relation relies on two auxiliary relations: the
_language building reduction relation_ $\longrightarrow_{\textsf{lan}}$, and
the _program reduction relation_ $\longrightarrow_{\textsf{exe}}$. Below we
describe the rules of Figure 4.

Rule (comm) is standard. Rule (comm-lang) handles the communication of
languages. In this rule, $\longrightarrow_{\textsf{lan}}^{*}$ is the reflexive
and transitive closure of $\longrightarrow_{\textsf{lan}}$. We evaluate $\ell$
to a language $\mathcal{L}$, and only then we perform the passing. Rule (comm-
trace) handles the communication of traces. Substitution
$P\\{\mathcal{L}/l\\}$ substitutes the free occurrences of $l$ in $P$ with
$\mathcal{L}$. Substitution $P\\{\mathfrak{T}/\textit{tr}\\}$ substitutes the
free occurrences of tr in $P$ with $\mathfrak{T}$. Both substitutions are
capture-avoiding, and their definition is straightforward, so we do not show
it.

Rule (exec) handles program executions when the language is available, that
is, it has been evaluated to some $\mathcal{L}$. This rule simply relies on
$\longrightarrow_{\textsf{exe}}$. Rule (exec-ctx) evaluates $\ell$ with
$\longrightarrow_{\textsf{lan}}$-reductions.

Rules (is-in-trace1) and (is-in-trace2) define the behavior of
$\mathtt{isInTrace}$. This process takes a step to $P$ if the label is in
$\mathfrak{T}$, and takes a step to $Q$ otherwise.

Rule (union) performs the union of two languages using the operation
$\cup_{\textsf{snx}}$. This operation adds new grammar productions and
inference rules to a language in the way that we have seen. This operation has
been previously defined in [6]. (We discuss related work in Section 6.) Rules
(union-ctx1) and (union-ctx2) evaluate the first and second argument of
$\mathtt{union}$, respectively.

Rule (program-step) handles program executions
$\texttt{(}\mathcal{L},\mathfrak{T}\texttt{)}\texttt{>}_{x}\;{t}$. This rule
is responsible for executing $t$ according to the operational semantics of
$\mathcal{L}$. To do so, we should query the inference rule system in
$\mathcal{L}$. However, $\mathcal{L}$ contains _syntax that represents_ an
inference system. We adopt the solution used in [6]: we translate the language
into a higher-order logic program with
$\llbracket{\mathcal{L}}\rrbracket^{\textsf{lp}}$, and we use the provability
relation $\models$ of logic programs to check whether a step from $t$ is
provable for some target $t^{\prime}$ and some label $t^{\prime\prime}$. The
translation $\llbracket{\mathcal{L}}\rrbracket^{\textsf{lp}}$ to logic
programs is easy, and has been described in [6]. The way this translation
works was not novel in there either, as it has been demonstrated previously
that inference systems of the like map well into logic programs [18, 12]. The
provability relation $\models$ comes directly from the semantics of higher
order logic programs, which can be found in [12]. Rule (program-step) also
appends $t^{\prime\prime}$ to the trace recorded in the program execution.

Rule (program-end) detects that a step is not provable for $t$. Then, the
execution of $t$ is terminated, and we send the trace over the channel $x$.

Notice that $t$ may fail to prove a step for several reasons, including that
$t$ is stuck because of missing reduction rules in an ill-defined language.
Programmers are responsible for giving well-designed languages, as Lang-n-Send
does not check that.

Reduction Semantics $P\equiv P$, $P\longrightarrow P$,
$\ell\longrightarrow_{\textsf{lan}}\ell$, $P\longrightarrow_{\textsf{exe}}P$

$\displaystyle P\mid\mathbf{0}\equiv P\qquad P\mid Q\equiv Q\mid P\qquad(P\mid
Q)\mid R\equiv P\mid(Q\mid R)\qquad!P\equiv P\mid!P$ $\displaystyle(\nu
x).\mathbf{0}\equiv\mathbf{0}\qquad(\nu x).(\nu y).P\equiv(\nu y).(\nu
x).P\qquad(\nu x).(P\mid Q)\equiv(\nu x).P\mid Q,~{}\textit{if $x$ is not a
free name of $Q$}$ (comm) $\displaystyle\displaystyle
x(y).P\mid\overline{x}\langle z\rangle.Q\longrightarrow P\\{z/y\\}\mid Q$
(comm-lang) $\displaystyle\displaystyle{\hbox{\hskip
12.67252pt\vbox{\hbox{\hskip-12.67252pt\hbox{\hbox{$\displaystyle\displaystyle\ell\longrightarrow_{\textsf{lan}}^{*}\mathcal{L}$}}}\vbox{}}}\over\hbox{\hskip
56.27895pt\vbox{\vbox{}\hbox{\hskip-56.27893pt\hbox{\hbox{$\displaystyle\displaystyle
x(l).P\mid\overline{x}\langle\ell\rangle.Q\longrightarrow
P\\{\mathcal{L}/l\\}\mid Q$}}}}}}$ (comm-trace) $\displaystyle\displaystyle
x(\textit{tr}).P\mid\overline{x}\langle\mathfrak{T}\rangle.Q\longrightarrow
P\\{\mathfrak{T}/\textit{tr}\\}\mid Q$ (exec)
$\displaystyle\displaystyle{\hbox{\hskip
30.33684pt\vbox{\hbox{\hskip-30.33684pt\hbox{\hbox{$\displaystyle\displaystyle\texttt{(}\mathcal{L},\mathfrak{T}\texttt{)}\texttt{>}_{x}\;t\longrightarrow_{\textsf{exe}}P$}}}\vbox{}}}\over\hbox{\hskip
28.01683pt\vbox{\vbox{}\hbox{\hskip-28.01683pt\hbox{\hbox{$\displaystyle\displaystyle\texttt{(}\mathcal{L},\mathfrak{T}\texttt{)}\texttt{>}_{x}\;t\longrightarrow
P$}}}}}}$ (exec-ctx) $\displaystyle\displaystyle{\hbox{\hskip
12.42801pt\vbox{\hbox{\hskip-12.42801pt\hbox{\hbox{$\displaystyle\displaystyle\ell\longrightarrow_{\textsf{lan}}\ell^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
40.69853pt\vbox{\vbox{}\hbox{\hskip-40.69853pt\hbox{\hbox{$\displaystyle\displaystyle\texttt{(}\ell,\mathfrak{T}\texttt{)}\texttt{>}_{x}\;t\longrightarrow\texttt{(}\ell^{\prime},\mathfrak{T}\texttt{)}\texttt{>}_{x}\;t$}}}}}}$
(is-in-trace1) $\displaystyle\displaystyle{\hbox{\hskip
50.85748pt\vbox{\hbox{\hskip-50.85748pt\hbox{\hbox{$\displaystyle\displaystyle\mathfrak{T}=t_{\\_}1\cdots
t_{\\_}n$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle 1\leq i\leq
n$}}}}\vbox{}}}\over\hbox{\hskip
59.56041pt\vbox{\vbox{}\hbox{\hskip-59.5604pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{isInTrace}(t_{\\_}i,\mathfrak{T})\Rightarrow
P~{};~{}Q\longrightarrow P$}}}}}}$ (is-in-trace2)
$\displaystyle\displaystyle{\hbox{\hskip
82.81033pt\vbox{\hbox{\hskip-82.81032pt\hbox{\hbox{$\displaystyle\displaystyle\mathfrak{T}=t_{\\_}1\cdots
t_{\\_}n$}\hskip 18.00003pt\hbox{\hbox{$\displaystyle\displaystyle
t\not=t_{\\_}i,\textit{ for all }1\leq i\leq n$}}}}\vbox{}}}\over\hbox{\hskip
56.16353pt\vbox{\vbox{}\hbox{\hskip-56.16353pt\hbox{\hbox{$\displaystyle\displaystyle\mathtt{isInTrace}(t,\mathfrak{T})\Rightarrow
P~{};~{}Q\longrightarrow Q$}}}}}}$ (union)
$\displaystyle\displaystyle\mathcal{L}_{\\_}1\;\mathtt{union}\;\mathcal{L}_{\\_}2\longrightarrow_{\textsf{lan}}\mathcal{L}_{\\_}1\cup_{\textsf{snx}}\mathcal{L}_{\\_}2$
(union-ctx1) $\displaystyle\displaystyle{\hbox{\hskip
20.70802pt\vbox{\hbox{\hskip-20.70802pt\hbox{\hbox{$\displaystyle\displaystyle\ell_{\\_}1\longrightarrow_{\textsf{lan}}\ell_{\\_}1^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
58.48811pt\vbox{\vbox{}\hbox{\hskip-58.48811pt\hbox{\hbox{$\displaystyle\displaystyle{\ell_{\\_}1}\;\mathtt{union}\;{\ell_{\\_}2}\longrightarrow_{\textsf{lan}}{\ell_{\\_}1^{\prime}}\;\mathtt{union}\;{\ell_{\\_}2}$}}}}}}$
(union-ctx2) $\displaystyle\displaystyle{\hbox{\hskip
20.70802pt\vbox{\hbox{\hskip-20.70802pt\hbox{\hbox{$\displaystyle\displaystyle\ell_{\\_}2\longrightarrow_{\textsf{lan}}\ell_{\\_}2^{\prime}$}}}\vbox{}}}\over\hbox{\hskip
58.48811pt\vbox{\vbox{}\hbox{\hskip-58.48811pt\hbox{\hbox{$\displaystyle\displaystyle{\ell_{\\_}1}\;\mathtt{union}\;{\ell_{\\_}2}\longrightarrow_{\textsf{lan}}{\ell_{\\_}1}\;\mathtt{union}\;{\ell_{\\_}2^{\prime}}$}}}}}}$
(program-step) $\displaystyle\displaystyle{\hbox{\hskip
30.0575pt\vbox{\hbox{\hskip-30.0575pt\hbox{\hbox{$\displaystyle\displaystyle\llbracket{\mathcal{L}}\rrbracket^{\textsf{lp}}\models(t\longrightarrow^{t^{\prime\prime}}t^{\prime})$}}}\vbox{}}}\over\hbox{\hskip
50.40453pt\vbox{\vbox{}\hbox{\hskip-50.40453pt\hbox{\hbox{$\displaystyle\displaystyle\texttt{(}\mathcal{L},{\mathfrak{T}}\texttt{)}\texttt{>}_{x}\;t\longrightarrow_{\textsf{exe}}\texttt{(}\mathcal{L},{{\mathfrak{T}}\;t^{\prime\prime}}\texttt{)}\texttt{>}_{x}\;t^{\prime}$}}}}}}$
(program-end) $\displaystyle\displaystyle{\hbox{\hskip
34.6825pt\vbox{\hbox{\hskip-34.6825pt\hbox{\hbox{$\displaystyle\displaystyle\llbracket{\mathcal{L}}\rrbracket^{\textsf{lp}}\not\models(t\longrightarrow^{t^{\prime\prime}}t^{\prime})$}}}\vbox{}}}\over\hbox{\hskip
38.7117pt\vbox{\vbox{}\hbox{\hskip-38.7117pt\hbox{\hbox{$\displaystyle\displaystyle\texttt{(}\mathcal{L},\mathfrak{T}\texttt{)}\texttt{>}_{x}\;{t}\longrightarrow_{\textsf{exe}}\overline{x}\langle\mathfrak{T}\rangle.\mathbf{0}$}}}}}}$

Figure 1: Reduction semantics of Lang-n-Send.

##  5 Examples

### Server Provides a Disrupt Operator

In this example, server is a server that offers two services: task and
quitOnFailureTask. These tasks are executed with BPA processes. However,
quitOnFailureTask is critical, and should stop if a mistake is detected. BPA
does not have a way to model disruptions. Therefore, at the moment of
executing quitOnFailureTask (and only in that case), server requests the piece
of operational semantics of the disrupt operator of LOTOS [10], adapted for
BPA in [3], and adds it to the language bpa from Section 2. Intuitively,
$P\blacktriangleright Q$ means that $P$ can be disrupted by $Q$. This process
behaves as $P$, though at any point, non-deterministically, $Q$ can start its
computation, which discards $P$ forever. We repeat the inference rules for
$\blacktriangleright$ ([3]).

$\displaystyle\inference{P_{\\_}1\longrightarrow^{a}\checkmark}{P_{\\_}1\blacktriangleright
P_{\\_}2\longrightarrow^{a}\checkmark}\quad\inference{P_{\\_}1\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}1^{\prime}}{P_{\\_}1\blacktriangleright
P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}1^{\prime}\blacktriangleright P_{\\_}2}$
$\displaystyle\inference{P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}2^{\prime}}{P_{\\_}1\blacktriangleright
P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}2^{\prime}}\quad\inference{P_{\\_}2\longrightarrow^{a}\checkmark}{P_{\\_}1\blacktriangleright
P_{\\_}2\longrightarrow^{a}\checkmark}$

We define the Lang-n-Send counterpart of $\blacktriangleright$ in two parts.
almostDisrupt contains the first row of the rules above. These rules define
the behavior of $\blacktriangleright$ insofar the preempted process is
concerned. disruptRules contains the second row of rules, which are for the
preempting process. Then, disrupt contains the union of the two, and is the
piece of language with the full definition of $\blacktriangleright$.

almostDisrupt $\triangleq$ $(Process\;P::=(\blacktriangleright\;P\;P),$
(checkMark A P1)(checkMark A (▶ P1 P2)) (⟶ A P1 P1’)(⟶ A (▶ P1 P2) (▶ P1’ P2))
)

disruptRules $\triangleq$
$(~{}~{}\inference{{(\longrightarrow\;A\;P_{\\_}2\;P_{\\_}2^{\prime})}}{(\longrightarrow\;A\;(\blacktriangleright\;P_{\\_}1\;P_{\\_}2)\;P_{\\_}2^{\prime})}\quad\inference{{(\textit{checkMark}\;A\;P_{\\_}2)}}{(\textit{checkMark}\;A\;(\blacktriangleright\;P_{\\_}1\;P_{\\_}2))}~{}~{})$

$\textit{disrupt}\triangleq\textit{almostDisrupt}\;\mathtt{union}\;\textit{disruptRule}$

Below, the process disruptOperatorProvider is a server, different from server,
that provides the disrupt piece of language over the channel getDisrupt. The
code for server is also below. We assume that bpa_program, a term, is a BPA
process to be executed for quitOnFailureTask, and that bpa_sorry is the BPA
process that can non-deterministically preempt bpa_program. For readability,
we use $\blacktriangleright$ in infix notation. The process for task is
irrelevant, and we chose $(\textit{act}\;(a))$.

$\textit{disruptOperatorProvider}\triangleq!(\overline{\textit{getDisrupt}}\langle\textit{disrupt}\rangle)$

$\begin{array}[]{ll}\textit{server}\triangleq&!(~{}\textit{task}(x).\texttt{(}\textit{bpa},[]\texttt{)}\texttt{>}_{x}\;(\textit{act}\;(a))\\\
&~{}~{}+\\\
&~{}~{}\textit{quitOnFailureTask}(x).\textit{getDisrupt}(l).\texttt{(}\textit{bpa\;$\mathtt{union}$\;l},[]\texttt{)}\texttt{>}_{x}\;(\textit{bpa\\_program}\blacktriangleright\textit{bpa\\_sorry})\;)\end{array}$

$\textit{system}\triangleq(\textit{server}\mid\textit{disruptOperatorProvider}\mid\textit{client}_{\\_}1\mid\textit{client}_{\\_}2\;\ldots\;\mid\textit{client}_{\\_}n)$

Suppose that bpa_sorry performs the action (sorry). We can detect whether
bpa_program has been disrupted with $\mathtt{isInTrace}$. The second branch of
the choice operator of server would be

$\textit{quitOnFailureTask}(x).\textit{getDisrupt}(l).(\nu x).\\\
\indent\indent\indent(\texttt{(}\textit{bpa\;$\mathtt{union}$\;l},[]\texttt{)}\texttt{>}_{x}\;(\textit{bpa\\_program}\blacktriangleright\textit{bpa\\_sorry})\mid
x(tr).\mathtt{isInTrace}((\textit{sorry}),tr)\Rightarrow
P_{\\_}1~{};~{}P_{\\_}2)$

Here, server creates a private channel $x$ over which the trace is sent. We
assume that $P_{\\_}1$ and $P_{\\_}2$ are two processes that server cares to
execute depending on whether (sorry) is in the trace or not.

### Server Decides Disrupt vs Interrupt

In this example, the server disruptOperatorProvider is called
quitModeProvider. It takes in input a channel (such as quitOnFailureTask), and
non-deterministically decides whether to provide the disrupt operator or the
interrupt operator $\rhd$ from [3]. The process $P\rhd Q$ means that $P$ can
be interrupted by $Q$. Differently from the disrupt operator, which completely
discards $P$ when $Q$ takes over, the interrupt operator resumes $P$ after $Q$
terminates.

bpa_program uses _one_ operator whose underlying semantics is given by
quitModeProvider. We fix the symbol for this operator to be
$\blacktriangleright$. Therefore, when quitModeProvider gives the interrupt
semantics, it does so by giving the rules of $\rhd$ for the symbol
$\blacktriangleright$. The piece of language for the preempted process,
almostDisrupt, is the same for $\blacktriangleright$ and $\rhd$. The rules for
the preempting process are the following ([3]).

$\displaystyle\inference{P_{\\_}2\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P_{\\_}2^{\prime}}{P_{\\_}1\rhd
P_{\\_}2\stackrel{{\scriptstyle a}}{{\longrightarrow}}P_{\\_}2^{\prime}\cdot
P_{\\_}1}\quad\inference{P_{\\_}2\longrightarrow^{a}\checkmark}{P_{\\_}1\rhd
P_{\\_}2\stackrel{{\scriptstyle a}}{{\longrightarrow}}P_{\\_}1}$

Below, interruptRules contains the Lang-n-Send counterpart of these rules,
though defined for the symbol $\blacktriangleright$, as explained above. When
we add interruptRules to almostDisrupt we obtain the full definition of the
interrupt operator (given as $\blacktriangleright$), which we call interrupt.

interruptRules $\triangleq$ (
$\inference{{(\longrightarrow\;A\;P_{\\_}2\;P_{\\_}2^{\prime})}}{(\longrightarrow\;A\;(\blacktriangleright\;P_{\\_}1\;P_{\\_}2)\;(\textit{seq}\;P_{\\_}2^{\prime}\;P_{\\_}1))}\quad\inference{{(\textit{checkMark}\;A\;P_{\\_}2)}}{(\longrightarrow\;A\;(\blacktriangleright\;P_{\\_}1\;P_{\\_}2)\;P_{\\_}1)}$
)

$\textit{interrupt}\triangleq\textit{almostDisrupt}\;\mathtt{union}\;\textit{interruptRules}$

$\textit{quitModeProvider}\triangleq~{}!\textit{whatTask}(y).(~{}\overline{\textit{getQuitMode}}\langle\textit{interrupt}\rangle\;+\;\overline{\textit{getQuitMode}}\langle\textit{disrupt}\rangle~{})$

$\begin{array}[]{ll}\textit{server}\triangleq{}&!(\textit{task}(x).\texttt{(}\textit{bpa},[]\texttt{)}\texttt{>}_{x}\;(\textit{act}\;(a))\\\
&~{}~{}+\\\
&~{}~{}\textit{quitOnFailureTask}(x).\overline{\textit{whatTask}}\langle\textit{quitOnFailureTask}\rangle.\textit{getQuitMode}(l).\\\
&\qquad\qquad\qquad\qquad\qquad\qquad\qquad\texttt{(}\textit{bpa\;$\mathtt{union}$\;l},[]\texttt{)}\texttt{>}_{x}\;(\textit{bpa\\_program}\blacktriangleright\textit{bpa\\_sorry})~{})\end{array}$

$\textit{system}\triangleq(\textit{server}\mid\textit{quitModeProvider}\mid\textit{client}_{\\_}1\mid\textit{client}_{\\_}2\;\ldots\;\mid\textit{client}_{\\_}n)$

### Server Decides Synchronous vs Asynchronous

In this example, the process client executes a CCS process called ccs_program.
However, client requests the semantics of the output prefix operator from the
server outputProvider, which decides, non-deterministically, whether
ccs_program must be executed synchronously or asynchronously. There is a
syntactic difference between the synchronous output $\overline{a}.P$ and the
asynchronous output $\overline{a}$ (with no continuation process). As
ccs_program is fixed, we settle to use the more general output form
$\overline{a}.P$, though its semantics will be given by the server.

We define a partial CCS with inaction, input prefix, output prefix, a one-
channel restriction operator $P\backslash a$, and the parallel operator. The
semantics of the output prefix, however, is not given. As we do not have
negative premises in rules, we define $P\backslash a$ by cases. For
simplicity, we only include channels $x$ and $y$.

$\begin{array}[]{l}\textit{Channel}\;a::=x\mid y\\\
\textit{Label}\;L::=\tau\mid a\mid\overline{a}\\\
\textit{Process}\;P::=\mathbf{0}\mid a.P\mid\overline{a}.P\mid~{}P\mid
P~{}\mid P\backslash a\\\\[1.93748pt] \end{array}$

$\displaystyle a.P\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P\quad\inference{P\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P^{\prime}}{P\backslash
a\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}P^{\prime}\backslash a}$
$\displaystyle\inference{P\stackrel{{\scriptstyle
y}}{{\longrightarrow}}P^{\prime}}{P\backslash x\stackrel{{\scriptstyle
y}}{{\longrightarrow}}P^{\prime}\backslash
x}\quad\inference{P\stackrel{{\scriptstyle\overline{y}}}{{\longrightarrow}}P^{\prime}}{P\backslash
x\stackrel{{\scriptstyle\overline{y}}}{{\longrightarrow}}P^{\prime}\backslash
x}\quad\inference{P\stackrel{{\scriptstyle
x}}{{\longrightarrow}}P^{\prime}}{P\backslash y\stackrel{{\scriptstyle
x}}{{\longrightarrow}}P^{\prime}\backslash
y}\quad\inference{P\stackrel{{\scriptstyle\overline{x}}}{{\longrightarrow}}P^{\prime}}{P\backslash
y\stackrel{{\scriptstyle\overline{x}}}{{\longrightarrow}}P^{\prime}\backslash
y}$ $\displaystyle\inference{P_{\\_}1\stackrel{{\scriptstyle
L}}{{\longrightarrow}}P_{\\_}1^{\prime}}{P_{\\_}1\mid
P_{\\_}2\stackrel{{\scriptstyle L}}{{\longrightarrow}}P_{\\_}1^{\prime}\mid
P_{\\_}2}\quad\inference{P_{\\_}2\stackrel{{\scriptstyle
L}}{{\longrightarrow}}P_{\\_}2^{\prime}}{P_{\\_}1\mid
P_{\\_}2\stackrel{{\scriptstyle L}}{{\longrightarrow}}P_{\\_}1\mid
P_{\\_}2^{\prime}}$

Below, partialCCS contains the Lang-n-Send counterpart of the partial CCS
defined above. Inaction is called nil, input prefix is called in, output
prefix is called out, the restriction operator is called res, and the parallel
operator is called par.

$\begin{array}[]{ll}\textit{partialCCS}\triangleq\\\
&(Channel\;a::=(\textit{x})\mid(\textit{y})\\\
&Label\;L::=(tau)\mid(\textit{in}\;a)\mid(\textit{out}\;a)\\\
&Process\;P::=(\textit{nil})\mid(\textit{in}\;a\;P)\mid(\textit{out}\;a\;P)\mid(\textit{res}\;a\;P)\mid(\textit{par}\;P\;P),\end{array}$

$\displaystyle{{(\longrightarrow\;(\textit{in}\;a)\;(\textit{in}\;a\;P)\;P)}}\quad\inference{{(\longrightarrow\;(tau)\;P\;P^{\prime})}}{(\longrightarrow\;(tau)\;(\textit{res}\;a\;P)\;(\textit{res}\;a\;P^{\prime}))}$
$\displaystyle\inference{{(\longrightarrow\;(\textit{in}\;(\textit{y}))\;P\;P^{\prime})}}{(\longrightarrow\;(\textit{in}\;(\textit{y}))\;(\textit{res}\;(\textit{x})\;P)\;(\textit{res}\;(\textit{x})\;P^{\prime}))}\quad\inference{{(\longrightarrow\;(\textit{out}\;(\textit{y}))\;P\;P^{\prime})}}{(\longrightarrow\;(\textit{out}\;(\textit{y}))\;(\textit{res}\;(\textit{x})\;P)\;(\textit{res}\;(\textit{x})\;P^{\prime}))}$
$\displaystyle\inference{{(\longrightarrow\;(\textit{in}\;(\textit{x}))\;P\;P^{\prime})}}{(\longrightarrow\;(\textit{in}\;(\textit{x}))\;(\textit{res}\;(\textit{y})\;P)\;(\textit{res}\;(\textit{y})\;P^{\prime}))}\quad\inference{{(\longrightarrow\;(\textit{out}\;(\textit{x}))\;P\;P^{\prime})}}{(\longrightarrow\;(\textit{out}\;(\textit{x}))\;(\textit{res}\;(\textit{y})\;P)\;(\textit{res}\;(\textit{y})\;P^{\prime}))}$
$\displaystyle\inference{{(\longrightarrow\;L\;P_{\\_}1\;P_{\\_}1^{\prime})}}{(\longrightarrow\;L\;(par\;P_{\\_}1\;P_{\\_}2)\;(par\;P_{\\_}1^{\prime}\;P_{\\_}2))}\quad\inference{{(\longrightarrow\;L\;P_{\\_}2\;P_{\\_}2^{\prime})}}{(\longrightarrow\;L\;(par\;P_{\\_}1\;P_{\\_}2)\;(par\;P_{\\_}1\;P_{\\_}2^{\prime}))}$

To complete partialCCS with synchronous output, we add the usual rule for
output prefix. To complete partialCCS with asynchronous output, we add 1) the
asynchronous output $\overline{a}$ to the grammar, added as
$(\textit{out}^{\prime}\;a)$ below, 2) its reduction rule
$\overline{a}\stackrel{{\scriptstyle\overline{a}}}{{\longrightarrow}}\mathbf{0}$,
and 3) the rule
$\overline{a}.P\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}(\overline{a}\mid
P)$111Notice that a simple rule like
$\overline{a}.P\stackrel{{\scriptstyle\tau}}{{\longrightarrow}}\overline{a}.\mathbf{0}\mid
P$ is problematic, as the rule applies to $\overline{a}.\mathbf{0}$, as well,
replicating forever. Also notice that this $\tau$-transition does not resolve
a choice, as partialCCS does not contain $+$. :

$\textit{synchOutput}\triangleq(~{}(\longrightarrow\;(\textit{out}\;a)\;(\textit{out}\;a\;P)\;P)~{})$
(* this rule is $\overline{a}.P\stackrel{{\scriptstyle
a}}{{\longrightarrow}}P$ *)

(⟶(

outa)(out′a)(nil))(⟶(tau)(outaP)(par(out′a)P))).

We give the definitions of outputProvider, client, and system below. When
ccs_program is the process
$(\overline{x}.y.\mathbf{0}\mid\overline{y}.\mathbf{0})\backslash x$, whether
a communication over the channel $y$ happens or not depends on whether
outputProvider sends synchOutput or asynchOutput.

$\textit{outputProvider}\triangleq!(~{}\,\overline{\textit{getOutput}}\langle\textit{synchOutput}\rangle\;+\;\overline{\textit{getOutput}}\langle\textit{asynchOutput}\rangle~{})$

$\textit{client}\triangleq\textit{getOutput}(l).\texttt{(}\textit{partialCCS}\;\mathtt{union}\;l,[]\texttt{)}\texttt{>}_{x}\;{\textit{ccs\\_program}}$

$\textit{system}\triangleq\textit{client}\mid\textit{outputProvider}$

##  6 Related Work

Our closest related work is [6]. Such work offers a $\lambda$-calculus with
first-class languages. We would like to characterize precisely the differences
between this paper and that work. This paper embeds language definitions in
the context of the $\pi$-calculus rather than the $\lambda$-calculus. The
syntax for languages, the language union operator, and the translation to
logic programs are from [6]. The operator for program executions, and rule
(program-step) are inspired by [6], but there are several differences in that
[6] does not allow for labeled transitions, and does not keep track of the
trace of the execution. Moreover, as a consequence of this latter remark, [6]
does not have operations such as $\mathtt{isInTrace}$, nor any other operation
for analyzing executions. Furthermore, [6] imposes that languages have a
notion of values, and successful program executions terminate ending up with a
value. This hardly applies to process algebras. [6] does not make any example
of concurrent scenarios. All the examples in this paper are new.

Semantics engineering tools allow programmers to define their own programming
languages [8, 19, 21]. Language workbenches [7] go even further in that
direction, and can automatically generate many components for the languages
being defined, such as editors with syntax colouring, highlighting,
completion, and reference resolution, and they assist in code generation, as
well as other phases. However, we are not aware of systems that allow pieces
of languages to be sent and received.

Multi-language operational semantics has been studied in several works.
Matthews and Findler provide a seminal work of this field [11]. Recent works
in multi-language semantics are [16, 17, 20]. All these works apply to two
languages selected beforehand, and do not handle arbitrary languages specified
by users. Furthermore, they do not offer a formal semantics of processes that
communicate languages.

##  7 Conclusion

We have presented Lang-n-Send, a $\pi$-calculus that is equipped with language
definitions. Processes can define languages, and use them to execute programs.
Moreover, processes can send and receive pieces of languages through channels.
We have presented a reduction semantics for Lang-n-Send.

We have offered examples that show that Lang-n-Send can express concurrent
scenarios that are not typical, where processes add language features based on
semantics sent by servers, and where they obtain which semantics their
operators adopt from servers. We believe that Lang-n-Send represents a first
step to a firm foundation for this type of programming.

In the future, we would like to extend Lang-n-Send. Indeed, we see Lang-n-Send
as a minimal foundational calculus that accommodates the communication of
languages. We purposely did not include operations that, in fact, are
interesting in this context. We plan to extend Lang-n-Send with more
operations on languages, such as removing rules, and renaming operators, as
well as more complex features such as converting languages from substitution-
based to environment-based, among others.

Adding binders to our language definitions does not seem to be problematic.
[6] has made that addition to model a $\lambda$-calculus as language
definition. We plan to use binders to make examples with the $\pi$-calculus
and its variants as Lang-n-Send language definitions.

We plan to add more operations that query traces more precisely, such as
counting labels in traces, and checking whether some labels appear before
others. We also plan to add primitive operations for slicing the traces
received [2], and we plan to add monitors to program executions [5].

Lang-n-Send does not allow for the term of a terminated program execution to
be sent. We have not included this feature because we believe that it enables
rather complex dynamics, and we wanted to confine our examples to the already
interesting scenarios that sending/receiving languages allow. We plan to
explore the sending of terms after execution as future work.

We plan to study more examples such as servers that decide the semantics of
the parallel operator for client processes (CCS style, only interleaving and
no communication, or the synchronous CSP parallel composition [9], for
instance). Another example is that of servers that decide the semantics of the
choice operator, such as internal vs external, among other possibilities.

Finally, we would like to study an appropriate notion of bisimilarity
equivalence in this context.

## References

  * [1]
  * [2] Hiralal Agrawal & Joseph R. Horgan (1990): _Dynamic Program Slicing_.  In: Proceedings of the ACM SIGPLAN 1990 Conference on Programming Language Design and Implementation, PLDI ’90, Association for Computing Machinery, New York, NY, USA, pp. 246–256, 10.1145/93542.93576.
  * [3] Jos C. M. Baeten & Jan A. Bergstra (2000): _Mode transfer in process algebra_.  Computing Science Reports 00-01, Technische Universiteit Eindhoven.
  * [4] Jan A. Bergstra & Jan W. Klop (1984): _Process Algebra for Synchronous Communication_.  Information and Control 60(1-3), pp. 109–137, 10.1016/S0019-9958(84)80025-X.
  * [5] Ian Cassar, Adrian Francalanza, Luca Aceto & Anna Ingólfsdóttir (2017): _A Survey of Runtime Monitoring Instrumentation Techniques_.  In: Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, PrePost@iFM 2017, Torino, Italy, 19 September 2017, pp. 15–28, 10.4204/EPTCS.254.2.
  * [6] Matteo Cimini (2021): _A Calculus for Multi-language Operational Semantics_.  In: Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers, pp. 25–42, 10.1007/978-3-030-95561-8_3.
  * [7] Sebastian Erdweg, Tijs Storm, Markus Völter, Meinte Boersma, Remi Bosman, WilliamR. Cook, Albert Gerritsen, Angelo Hulshout, Steven Kelly, Alex Loh, Gabriël D. P. Konat, PedroJ. Molina, Martin Palatnik, Risto Pohjonen, Eugen Schindler, Klemens Schindler, Riccardo Solmi, Vlad A. Vergu, Eelco Visser, Kevin Vlist, Guido H. Wachsmuth & Jimi Woning (2013): _The State of the Art in Language Workbenches_.  In Martin Erwig, Richard F. Paige & Eric Wyk, editors: Software Language Engineering, Lecture Notes in Computer Science 8225, Springer, pp. 197–217, 10.1007/978-3-319-02654-111.
  * [8] Matthias Felleisen, Robert Bruce Findler & Matthew Flatt (2009): _Semantics Engineering with PLT Redex_ , 1st edition.  The MIT Press.
  * [9] C.A.R. Hoare (1985): _Communicating Sequential Processes_.  Prentice-Hall International Series in Computer Science, Prentice Hall.  Available at http://www.usingcsp.com/cspbook.pdf.
  * [10] ISO/IEC (1989): _LOTOS — a formal description technique based on the temporal ordering of observational behaviour_.  ISO IS 8807, 10.3403/00230466U.
  * [11] Jacob Matthews & Robert Bruce Findler (2007): _Operational Semantics for Multi-Language Programs_.  In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’07, Association for Computing Machinery, New York, NY, USA, p. 3–10, 10.1145/1190216.1190220.
  * [12] Dale Miller & Gopalan Nadathur (2012): _Programming with Higher-Order Logic_ , 1st edition.  Cambridge University Press, New York, NY, USA, 10.1017/CBO9781139021326.
  * [13] Robin Milner, Joachim Parrow & David Walker (1992): _A calculus of mobile processes, I_.  Information and Computation 100(1), pp. 1–40, 10.1016/0890-5401(92)90008-4.
  * [14] Robin Milner, Joachim Parrow & David Walker (1992): _A calculus of mobile processes, II_.  Information and Computation 100(1), pp. 41–77, 10.1016/0890-5401(92)90009-5.
  * [15] Peter D. Mosses (2008): _Component-Based Description of Programming Languages_.  In: Visions of Computer Science - BCS International Academic Conference, Imperial College, London, UK, 22-24 September 2008, pp. 275–286, 10.14236/ewic/VOCS2008.23.
  * [16] Daniel Patterson & Amal Ahmed (2017): _Linking Types for Multi-Language Software: Have Your Cake and Eat It Too_.  In Benjamin S. Lerner, Rastislav Bodík & Shriram Krishnamurthi, editors: 2nd Summit on Advances in Programming Languages (SNAPL 2017), Leibniz International Proceedings in Informatics (LIPIcs) 71, Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, pp. 12:1–12:15, 10.4230/LIPIcs.SNAPL.2017.12.
  * [17] Daniel Patterson, Jamie Perconti, Christos Dimoulas & Amal Ahmed (2017): _FunTAL: Reasonably Mixing a Functional Language with Assembly_.  In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Association for Computing Machinery, New York, NY, USA, pp. 495–509, 10.1145/3062341.3062347.
  * [18] Frank Pfenning & Carsten Schürmann (1999): _System Description: Twelf - A Meta-Logical Framework for Deductive Systems_.  In: Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, CADE-16, Springer-Verlag, Berlin, Heidelberg, pp. 202–206, 10.1007/3-540-48660-714.
  * [19] Grigore Rosu & Traian F. Şerbănuţă (2010): _An overview of the K semantic framework_.  The Journal of Logic and Algebraic Programming 79(6), pp. 397–434, 10.1016/j.jlap.2010.03.012.
  * [20] Gabriel Scherer, Max S. New, Nick Rioux & Amal Ahmed (2018): _Fabulous Interoperability for ML and a Linear Language_.  In: Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, pp. 146–162, 10.1007/978-3-319-89366-2_8.
  * [21] Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar & Rok Strniša (2007): _Ott: Effective Tool Support for the Working Semanticist_.  In: Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP ’07, ACM, New York, NY, USA, pp. 1–12, 10.1145/1291151.1291155.