Towards Reversible Computation in Erlang⋆
Naoki Nishida1 , Adrián Palacios2,⋆⋆ , and Germán Vidal2

arXiv:1608.05521v1 [cs.PL] 19 Aug 2016

1

Graduate School of Information Science, Nagoya University
Furo-cho, Chikusa-ku, 4648603 Nagoya, Japan,
nishida@is.nagoya-u.ac.jp
2
MiST, DSIC, Universitat Politècnica de València
Camino de Vera, s/n, 46022 Valencia, Spain
{apalacios, gvidal}@dsic.upv.es

Abstract. In a reversible language, any forward computation can be
undone by a finite sequence of backward steps. Reversible computing
has been studied in the context of different programming languages and
formalisms, where it has been used for debugging and for enforcing faulttolerance, among others. In this paper, we consider a subset of Erlang,
a concurrent language based on the actor model. We formally introduce
a reversible semantics for this language. To the best of our knowledge,
this is the first attempt to define a reversible semantics for Erlang.

1

Introduction

Let us consider that the operational semantics of a programming language is
specified by a state transition relation R such that R(s, s′ ) holds if the state
s′ is reachable—in one step—from state s. As it is common practice, we let R∗
denote the reflexive and transitive closure of R. Then, we say that a programming
language (or formalism) is reversible if there exists a constructive algorithm that
can be used to, given a computation from state s to state s′ , in symbols R∗ (s, s′ ),
obtain the state s from s′ . In general, such a property does not hold for most
programming languages and formalisms. We refer the interested reader to, e.g.,
[3, 10, 23, 24] for a high level account of the principles of reversible computation.
The notion of reversible computation was first introduced in Landauer’s seminal work [13] and, then, further improved by Bennett [2] in order to avoid the
generation of “garbage” data. The idea underlying these works is that any programming language or formalism can be made reversible by adding the history of
the computation to each state, which is usually called a Landauer’s embedding.
⋆

⋆⋆

This work has been partially supported by the EU (FEDER) and the Spanish Ministerio de Economı́a y Competitividad (MINECO) under grant TIN2013-44742-C4-1-R
and by the Generalitat Valenciana under grant PROMETEO-II/2015/013 (SmartLogic). The second and third authors also acknowledge a partial support of COST
Action IC1405 on Reversible Computation - extending horizons of computing.
Partially supported by the the EU (FEDER) and the Spanish Ayudas para contratos
predoctorales para la formación de doctores de la Secretarı́a de Estado de Investigación, Desarrollo e Innovación del MINECO under FPI grant BES-2014-069749.

Although carrying the history of a computation might seem infeasible because
of its size, there are several successful proposals that are based on this idea. In
particular, one can restrict the original language or apply a number of analysis
in order to restrict the required information in the history as much as possible,
as in, e.g., [17, 18, 21] in the context of a functional language.
Alternatively, one can consider a restricted language where computations are
reversible without adding any additional information to the states. This is the
case, e.g., of the functional language considered in [25] or the language Janus (see
[23] and references therein). Obviously, such languages are not universal since
there are functions that cannot be represented (e.g., non-injective functions).
In this paper, we consider the former approach, the so-called Landauer’s
embedding. In particular, we aim at introducing a form of reversibility in the
context of a programming language that follows the actor model (concurrency
based on message passing), and that can be considered as a subset of the concurrent and functional language Erlang [1]. Previous approaches have mainly
considered reversibility in—mostly synchronous—concurrent calculi like CCS [7,
8], a general framework for reversibility of algebraic process calculi [19], or the
recent approach to reversible session-based π-calculus [22]. However, we can only
find a few approaches that considered the reversibility of asynchronous calculi,
e.g., Cardelli and Laneve’s reversible structures [5] or the approach based on a
rollback construct of [11, 14–16] for a higher-order asynchronous π-calculus.
To the best of our knowledge, our work is the first one that considers reversibility in the context of the functional, concurrent, and distributed language
Erlang. Here, given a running Erlang system consisting of a pool of interacting
processes, possibly distributed in several computers, we aim at allowing a single
process to undo its actions, including the interactions with other processes, following a rollback fashion. In this context, we must ensure causal consistency [7],
i.e., an action cannot be undone until all the actions that depend on it have been
already undone. E.g., if a process spawns another process, we cannot undo this
process spawning until all the actions performed by the new process are undone
too. This is particularly challenging in our asynchronous and distributed setting
since there is no global order for the language events. In this paper, we introduce
a rollback operator that undoes the actions of a process until a checkpoint is
reached. This could be considered as a promising basis for defining safe sessions
in a language like Erlang.
In this paper, we consider a simple Erlang-like language that can be considered a subset of Core Erlang [6]. We present the following contributions: First,
we introduce an appropriate standard semantics for the language. In contrast
to monolothic previous semantics like that in [4], our semantics is more modular, which simplifies the definition of a reversible extension. In contrast to [20],
although we follow some of the ideas in this approach (e.g., the use of a global
mailbox), we include the evaluation of expressions and, moreover, our treatment
of messages is more deterministic.3 We then introduce a reversible extension
3

E.g., in the semantics of [20], at the expression level, the transition semantics of
an expression containing a receive statement is, in principle, infinitely branching,

::=
::=
::=
::=
::=
|
|
|
|
clause ::=
pat ::=

Module
fun
fname
lit
expr

module Atom = fun 1 , . . . , fun n
fname = fun (X1 , . . . , Xn ) → expr
Atom/Integer
Atom | Integer | F loat | [ ]
Var | lit | fname | [expr1 |expr2 ] | {expr1 , . . . , exprn }
call expr (expr1 , . . . , exprn ) | apply expr (expr1 , . . . , exprn )
case expr of clause1 ; . . . ; clausem end
let Var = expr1 in expr2 | receive clause1 ; . . . ; clausen end
spawn(expr, [expr1 , . . . , exprn ]) | expr1 ! expr2 | self()
pat when expr1 → expr2
Var | lit | [pat1 |pat2 ] | {pat1 , . . . , patn }
Fig. 1. Language syntax rules

of the standard semantics (basically, a Landauer’s embedding). Here, we focus
only on the concurrent actions (namely, process spawning, message sending and
receiving) and, thus, do not consider the reversibilization of the functional component of the language; rather, we assume that the state of the process—the
current expression and its environment—is stored in the history after each execution step. This approach could be improved following, e.g., the approaches
from [17, 18, 21]. Finally, we introduce a backward semantics that can be used
to undo the actions of a given process in a rollback fashion, until a checkpoint—
introduced by the programmer—is reached. Here, ensuring causal consistency is
essential and might propagate the rollback action to other, dependent processes.

2

Language Syntax

In this section, we present the syntax of a first-order concurrent and distributed
functional language that follows the actor model. Our language is basically equivalent to a subset of Core Erlang [6].
The syntax of the language can be found in Figure 1. Here, a module is a
sequence of function definitions, where each function name f /n (atom/arity)
has an associated definition of the form fun (X1 , . . . , Xn ) → e. We consider that
a program consists of a single module for simplicity. The body of a function
is an expression, which can include variables, literals, function names, lists, tuples, calls to built-in functions—mainly arithmetic and relational operators—,
function applications, case expressions, let bindings, and receive expressions; furthermore, we also consider the functions spawn, “!” (for sending a message), and
self() that are usually considered built-in’s in the Erlang language.
Despite the general syntax in Figure 1, as mentioned before, we only consider
first order expressions. Therefore, the first expression in calls, applications and
spawns can only be function names (instead of arbitrary expressions or closures).
In this language, we distinguish expressions, patterns, and values. As mentioned before, expressions can include all constructs of the language. In contrast,
since their formulation allows for an infinite number of possible queues and selected
messages.

patterns are built from variables, literals, lists, and tuples. Finally, values are
built from literals, lists, and tuples, i.e., they are ground —without variables—
patterns. Expressions are denoted by e, e′ , e1 , e2 , . . ., patterns by p, p′ , p1 , p2 , . . .
and values by v, v ′ , v1 , v2 , . . . As it is common practice, a substitution θ is a mapping from variables to expressions such that Dom(θ) = {X ∈ Var | X 6= θ(X)}
is its domain. Substitutions are usually denoted by sets of mappings like, e.g.,
{X1 7→ v1 , . . . , Xn 7→ vn }. Substitutions are extended to morphisms from expressions to expressions in the natural way. The identity substitution is denoted
by id. Composition of substitutions is denoted by juxtaposition, i.e., θθ′ denotes a substitution θ′′ such that θ′′ (X) = θ′ (θ(X)) for all X ∈ Var. Also,
we denote by θ[X1 7→ v1 , . . . , Xn 7→ vn ] the update of θ with the mapping
X1 7→ v1 , . . . , Xn 7→ vn , i.e., it denotes a new substitution θ′ such that θ′ (X) = vi
if X = Xi , for some i ∈ {1, . . . , n}, and θ′ (X) = θ(X) otherwise.
In a case expression “case e of p1 when e1 → e′1 ; . . . ; pn when en → e′n end”,
we first evaluate e to a value, say v; then, we should find (if any) the first clause
pi when ei → e′i such that v matches pi (i.e., there exists a substitution σ for the
variables of pi such that v = pi σ) and ei σ—the guard —reduces to true; then,
the case expression reduces to e′i σ. Note that guards can only contain calls to
built-in functions (typically, arithmetic and relational operators).
As for the concurrent features of the language, we consider that a system
is of a pool of processes that can only interact through message sending and
receiving (i.e., there is no shared memory). Each process has an associated pid
(process identifier), which is unique in a system. For clarity, we often denote
pids with roman letters p, p′ , p1 , . . ., though they are considered values in our
language (i.e., atoms). By abuse of notation, when no confusion can arise, we
refer to a process with its pid.
An expression of the form spawn(f /n, [e1 , . . . , en ]) has, as a side effect, the
creation of a new process with a fresh pid p which is initialized with the expression apply f /n (e1 , . . . , en ); the expression spawn(f /n, [e1 , . . . , en ]) itself evaluates to the new pid p. The function self() just returns the pid of the current
process. An expression of the form p ! v evaluates to the value v and, as a side
effect, stores the value v—the message—in the queue or mailbox of process p.
Finally, an expression “receive p1 when e1 → e′1 ; . . . ; pn when en → e′n end”
traverses the messages in the process’ queue until one of them matches a branch
in the receive statement; i.e., it should find the first message v in the process’
queue (if any) such that case v of p1 when e1 → e′1 ; . . . ; pn when en → e′n end
can be reduced; then, the receive expression evaluates to the same expression
to which the above case expression would be evaluated, with the additional side
effect of deleting the message v from the process’ queue. If there is no matching message in the queue, the process suspends its execution until a matching
message arrives.
Example 1. Consider the program shown in Figure 2, where the symbol “ ” is
used to denote an anonymous variable, i.e., a variable whose name is not relevant.
The computation starts with “apply main/0 ().” Then, this process, say P 1,
spawns two new processes, say P 2 and P 3, and then sends the message “world”

main/0 = fun () → let P 2 = spawn(echo/0, [ ])
in let P 3 = spawn(target/0, [ ])
in let = P 3 ! world
in let P 2 ! {P 3, hello}

P1 ▼
▼

world

▼▼▼
▼
{P 3,hello} &&

P2

// P 3
q88
q
q
qqqhello

target/0 = fun () → receive
A → receive
echo/0 = fun () → receive
B → {A, B}
{P, M } → P ! M
end
end
end
Fig. 2. A simple concurrent program

to process P 3 and the message {P 3, hello} to process P 2, which then resends
“hello” to P 3. In our language, there is no guarantee regarding which message
arrives first to P 3, i.e., “apply main/0 ()” can evaluate nondeterministically to
either {hello, world} or {world, hello}. This is coherent with the semantics of
Erlang, where the only guarantee is that if two messages are sent from process
p to process p′ and both are delivered, then the order of these messages is kept.

3

The Language Semantics

In order to set precisely the framework for our proposal, in this section we
formalize the semantics of the considered language.
Definition 1 (process). A process is denoted by a tuple of the form hp, (θ, e), qi
where p is the pid of the process, (θ, e) is the control of the state—which consists
of an environment (a substitution) and an expression to be evaluated—, and q
is the process’ mailbox, a FIFO queue with the sequence of messages that have
been sent to the process.
A running system is then a pool of processes, which is formally defined as follows:
Definition 2 (system). A system is denoted by Γ ; Π, where Γ is a global mailbox of the system (see below) and Π is a pool of processes, denoted by an expression of the form hp1 , (θ1 , e1 ), q1 i & · · · & hpn , (θn , en ), qn i, where “&” is an associative and commutative operator. We typically denote a system by an expression
of the form Γ ; hp, (θ, e), qi&Π to point out that hp, (θ, e), qi is an arbitrary process of the pool (thanks to the fact that “&” is associative and commutative).
The role of Γ (which is similar to the “ether” in [20]) will be clarified later,
but it is essential to guarantee that all admissible interleavings can be modelled with the semantics. Here, we define Γ as a set of FIFO queues among
all (non-necessarily different) pids, i.e., Γ is made of elements of the form
(p, q, [v1 , . . . , vn ]), where p, q are (not necessarily different) pids and [v1 , . . . , vn ]
is a (possibly empty) ordered list of messages such that v1 is the oldest message and vn is the most recent one. For simplicity, we assume that Γ is initialized as follows: {(p, q, [ ]) | p, q are pids}. Then, we use the following notation:

ℓ

(Var )

θ, ei −→ θ′ , e′i

(Tuple)

τ

θ, X −→ θ, θ(X)

ℓ

θ, {e1 , . . . , en } −→
ℓ

(List1 )

i ∈ {1, . . . , n}
θ′ , {e

′
1,i−1 , ei , ei+1,n }

ℓ

θ, e1 −→ θ′ , e′1
ℓ

θ, [e1 |e2 ] −→ θ′ , [e′1 |e2 ]

(List2 )

θ, e2 −→ θ′ , e′2
ℓ

θ, [e1 |e2 ] −→ θ′ , [e1 |e′2 ]

ℓ

(Let1 )

θ, e1 −→ θ′ , e′1
ℓ

θ, let X = e1 in e2 −→ θ′ , let X = e′1 in e2

(Let2 )

ℓ

(Case1 )

θ, e −→ θ′ , e′
θ, case e of cl1 ; . . . ; cln end

(Case2 )

τ

θ, let X = v in e −→ θ[X 7→ v], e

match(v, cl1 , . . . , cln ) = hθi , ei i
τ

θ, case v of cl1 ; . . . ; cln end −→ θθi , ei

ℓ

−→ θ′ , case e′ of cl1 ; . . . ; cln end
ℓ

(Call1 )

θ, ei −→ θ′ , e′i
ℓ

θ, call op (en ) −→

i ∈ {1, . . . , n}

θ′ , call

op

(e1,i−1 , e′i , ei+1,n )
ℓ

(Apply1 )

(Apply2 )

θ, ei −→ θ′ , e′i

(Call2 )

eval(op, v1 , . . . , vn ) = v
τ

θ, call op (v1 , . . . , vn ) −→ θ, v

i ∈ {1, . . . , n}

ℓ

θ, apply a/n (en ) −→ θ′ , apply a/n (e1,i−1 , e′i , ei+1,n )
µ(a/n) = fun (X1 , . . . , Xn ) → e
τ

θ, apply a/n (v1 , . . . , vn ) −→ {X1 7→ v1 , . . . , Xn 7→ vn }, e

Fig. 3. Standard semantics: evaluation of sequential expressions

Γ ∪ (p, q, v) denotes Γ \ {(p, q, vs)} ∪ {(p, q, vs++[v]}, while Γ \ (p, q, v) denotes
Γ \ {(p, q, v : vs)} ∪ {(p, q, vs)}, where ++ is the list concatenation operator.
In the following, we denote by on the sequence of syntactic objects o1 , . . . , on
for some n. We also write oi,j for the sequence oi , . . . , oj when i ≤ j (and the
empty sequence otherwise). We write o when the number of elements is not
relevant.
The semantics is defined by means of two transition relations: −→ for expressions and 7−→ for systems. Let us first consider the labelled transition relation
−→ : (Env, Exp) × Label × (Env, Exp)
where Env and Exp are the domains of environments (i.e., substitutions) and
expressions, respectively, and Label denotes an element of the set
{τ, send(v1 , v2 ), rec(y, cln ), spawn(y, a/n, [en]), self(y)}
whose meaning will be explained below. For clarity, we divide the transition
rules of the semantics for expressions in two sets, depicted in Figures 3 and 4
for sequential and concurrent expressions, respectively.
Most of the rules are self-explanatory. In the following, we only discuss some
subtle or complex issues. In principle, the transitions are labelled either with
τ (a sequential expression) or with a label that identifies a concurrent action.
Labels are used in the system rules (Figure 5) to perform the associated side
effects.

(Send1 )

θ, e1 −→ θ′ , e′1

ℓ

θ, e2 −→ θ′ , e′2

ℓ

θ, e1 ! e2 −→ θ′ , e1 ! e′2

ℓ

θ, e1 ! e2 −→ θ′ , e′1 ! e2

(Send2 )
θ, v1 ! v2

ℓ

send(v1 ,v2 )

−→

(Receive)
θ, receive cl1 ; . . . ; cln end
(Spawn)
θ, spawn(a/n, [e1 , . . . , en ])
(Self )

θ, v2
rec(y,cln )

−→

θ, y

spawn(y,a/n,[en ])

−→

θ, y

self(y)

θ, self() −→ θ, y
Fig. 4. Standard semantics: evaluation of concurrent expressions

In some of the rules (e.g., for evaluating tuples, lists, etc) we consider for
simplicity that elements are evaluated in a non-deterministic way. In an actual
programming language the order of evaluation of the arguments in the tuple or
list is usually fixed. E.g., in Erlang, reduction takes place from left to right.
For case evaluation, we assume an auxiliary function match which selects the
first clause, cli = (pi when e′i → ei ), such that v matches pi , i.e., v = θi (pi ), and
the guard holds, i.e., θθi , e′i −→∗ θ′ , true. Note that, for simplicity, we do not
consider here the case in which the argument v matches no clause.
Function calls can either be defined in the program (apply) or be a built-in
(call). In the latter case, they are evaluated using the auxiliary function eval. In
rule Apply2 , we consider that the mapping µ stores all function definitions, i.e.,
it maps every function name a/n to its definition fun (X1 , . . . , Xn ) → e in the
program. As for the applications, note that we only consider first-order functions.
In order to extend our semantics to also consider higher-order functions, one
should reduce the function name to a closure of the form (θ′ , fun (X1 , . . . , Xn ) →
e) and, then, reduce e in the environment θ′ [X1 7→ v1 , . . . , Xn 7→ vn ]. We skip
this extension since it is orthogonal to our approach.
Let us now consider the evaluation of concurrent expressions that produce
some side effect (Figure 4). Here, we can distinguish two kinds of rules. On
the one hand, we have the rules for “!”, Send1 and Send2 . In this case, we
know locally what the expression should be reduced to (i.e., v2 in rule Send2 ).
For the remaining rules, this is not known locally and, thus, we return a fresh
distinguished symbol, y 6∈ Var (by abuse, y is dealt with as a variable), so that
the system rules will eventually bind y to its correct value. This trick allows us to
keep the rules for expressions and systems separated (i.e., the semantics shown in
Figures 3 and 4 is mostly independent from the rules in Figure 5), in contrast to
other calculi, e.g., [4], where they are combined into a single transition relation.
Let us finally consider the system rules, which are depicted in Figure 5. In
most of the rules, we consider an arbitrary system of the form Γ ; hp, (θ, e), qi&Π,
where Γ is the global mailbox and hp, (θ, e), qi&Π is a pool of process that
contains at least one process hp, (θ, e), qi.

τ

(Exp)

θ, e → θ′ , e′
Γ ; hp, (θ, e), qi&Π 7−→ Γ ; hp, (θ′ , e′ ), qi&Π

(Send )

θ, e
→
θ ′ , e′
Γ ; hp, (θ, e), qi&Π 7−→ Γ ∪ (p, p′′ , v); hp, (θ′ , e′ ), qi&Π

(Receive)

θ, e → θ′ , e′ matchrec(cln , q) = (θi , ei , q ′ )
Γ ; hp, (θ, e), qi&Π 7−→ Γ ; hp, (θ′ θi , e′ {y 7→ ei }), q ′ i&Π

(Spawn)

θ, e
→
θ′ , e′ p′ is a fresh pid
′
′
Γ ; hp, (θ, e), qi&Π 7−→ Γ ; hp, (θ , e {y →
7 p′ }), qi&hp′ , (θ′ , apply a/n (e1 , . . . , en )), [ ]i&Π

send(p′′ ,v)

rec(y,cln )

spawn(y,a/n,[en ])

self(y)

(Self )

(Sched )

θ, e → θ′ , e′
Γ ; hp, (θ, e), qi&Π 7−→ Γ ; hp, (θ′ , e′ {y 7→ p}), qi&Π
α(Γ ) = (p′ , p) Π = hp, (θ, e), qi&Π ′
Γ ; Π 7−→ Γ \ {(p′ , p, v)}; hp, (θ, e), v : qi&Π ′
Fig. 5. Standard semantics: system rules

Note that, in rule Send , we add the triple (p, p′′ , v) to Γ instead of adding
it to the queue of process p′′ . This is necessary to ensure that all possible nondeterministic results can be obtained (as discussed in Example 1). Observe that
e′ is usually different from v since e may have different nested operators. E.g., if
e has the form “case p ! v of {. . .},” then e′ will be “case v of {. . .}” with label
send(p, v).
In rule Receive, we use the auxiliary function matchrec to evaluate a receive
expression. The main difference with match is that matchrec also takes a queue q
and returns the modified queue q ′ . Then, the distinguished variable y is bound to
the expression in the selected clause, ei , and the environment is extended with
the matching substitution. If no message in the queue q matches any clause,
then the rule is not applicable and the selected process cannot be reduced (i.e.,
it suspends).
With the rules presented so far, any system will soon reach a state in which no
reduction can be performed, since messages are stored in the global mailbox, but
they are not dispatched to the queues of the processes. This is precisely the task
of the scheduler, which is modelled by rule Sched . The rule is non-deterministic,
so any scheduling policy can be modelled by the semantics. A message is selected
from the list of messages by the auxiliary function α, which can select any
arbitrary pair of (non-necessarily different) pids (p′ , p). Note that we take the
oldest message in the queue—the first one in the list—, which is necessary to
ensure that “the messages sent—directly—between two given processes arrive in
the same order they were sent”, as mentioned in the previous section.
Example 2. Let us consider the program shown in Figure 6 and a possible execution trace. This trace is modelled by our semantics. For clarity, we only show

main/0
main/0 = fun () → let S = spawn(server/0, [ ])
in let = spawn(client/1, [S])
in apply client/1 (S)

spawn
spawn

client1

client/1 = fun (S) → let = S ! {self(), req}
in receive
ack → ok
end

server
receive

server/0 = fun () → receive
{P, M} → let = P ! ack
in apply server/0 ()
end

##

++

client2

oo

client2 ! ack
server ! req
receive

oo

ok

//

receive

server ! req

//

receive
ok

client1 ! ack
receive

Fig. 6. A simple client-server
7−→
7−→
7−→
7−→
7−→
7−→
7−→
7−→
7−→
7−→
7−→

[ ]; hc1, (id, apply main/0 ()), [ ]i
...
[ ]; hc1, (σ, let = S ! {c1, req} in . . .), [ ]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i
[(c1, s, [v2 ])]; hc1, (σ, let = {c1, req} in . . .), [ ]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i
[(c1, s, [v2 ])]; hc1, (σ, receive ack → . . .), [ ]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i
[ ]; hc1, (σ, receive ack → . . .), [ ]i & hs, (id, receive {P, M} → . . .), [{c1, req}]i &
hc2, (σ, ok), [ ]i
[ ]; hc1, (σ, receive ack → . . .), [ ]i & hs, (θ2 , let = P ! ack in . . .), [{c1, req}]i &
hc2, (σ, ok), [ ]i
[(s, c1, [ack])]; hc1, (σ, receive ack → . . .), [ ]i & hs, (θ2 , let = ack in . . .), [{c1, req}]i &
hc2, (σ, ok), [ ]i
[(s, c1, [ack])]; hc1, (σ, receive ack → . . .), [ ]i & hs, (θ2 , apply server/0 ()), [ ]i &
hc2, (σ, ok), [ ]i
[(s, c1, [ack])]; hc1, (σ, receive ack → . . .), [ ]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i
[ ]; hc1, (σ, receive ack → . . .), [ack]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i
[ ]; hc1, (σ, ok), [ ]i & hs, (id, receive {P, M} → . . .), [ ]i &
hc2, (σ, ok), [ ]i

Fig. 7. A trace with σ = {S 7→ s}, θ2 = {P 7→ c1, M 7→ req}, and v2 = {c1, req}.

in Figure 7 the transition steps that correspond to the last two messages sent
between client1 and server .

4

Reversible Semantics

In this section, we introduce a reversible extension of the semantics defined so
far. Moreover, thanks to our modular design, the semantics for the language
expressions needs not be changed.
To be precise, in this section we introduce two transition relations: ⇀ and ↽.
The first relation, ⇀, is a conservative extension of the standard semantics 7−→
(Figure 5) to also include some additional information in the states, following a
typical Landauer’s embedding. We refer to ⇀ as the forward reversible semantics
(or simply the forward semantics). In contrast, the second relation, ↽, proceeds
in the backwards direction, “undoing” the actions of a single process (and, by

causal consistency, possibly propagating it to other processes). We refer to ↽
as the backward (reversible) semantics. Finally, we denote the union ⇀ ∪ ↽
by ⇋. Then, in a computation modelled with ⇋ the system mainly evolves
forwards, except for some processes that can run backwards in order to undo
some particular actions (and, afterwards, will run forwards again).
Here, we will introduce a (non-deterministic) “undo” operation (cf. rules
Undo1 and Undo2 in Figure 10) which has some similarities to, e.g., the rollback
operator of [11]. In order to delimit the scope of this operation (i.e., to determine
when to stop undoing the actions of a process), we allow the programmer to
introduce checkpoints in a program. Syntactically, they are denoted with the
built-in function check, which is used in a let expression as follows: “let =
check in expr”. Function check returns an identifier t associated to the checkpoint
(see below). In the following, we consider that the rules to evaluate the language
expressions (Figures 3 and 4) are extended with the following rule:
(Check )

check(y)

θ, check −→ θ, y
In the next section, we will see that the only effect of a call to function check is
to add a checkpoint in the trace of a given process.
4.1

Forward Semantics

First, we introduce the forward (reversible) semantics. Since the expression rules
are the same (except for the additional rule for check mentioned above), we will
only introduce the reversible system rules, which are shown in Figure 8. Processes
now include a memory π that records the intermediate states of a process. Note
that we could optimize this in order to follow a strategy similar to that in [17,
18, 21] for the reversibility of functional expressions, but this is orthogonal to
our purpose in this paper, so we focus only on the concurrent actions.
The rules are mostly self-explanatory. Here, we use a special symbol #tk for
checkpoints, where k denotes the type of checkpoint and t is a (unique) identifier
for the checkpoint. The checkpoints introduced by the programmer, denoted by
#tch , represent a safe point in the program execution, i.e., if we are undoing
the actions of a given process, we can safely stop the backward computation at
any checkpoint. Rollback operations (i.e., rules Undo1 and Undo2 in Figure 10)
and checkpoints introduced by the programmer lay the ground for defining safe
sessions whose actions can be undone if, e.g., an exception occurs before they
are completed. In practice, we distinguish three types of checkpoints:
– Checkpoints introduced by the programmer. These checkpoints correspond
to the evaluation of function check and are denoted with #ch .
– Checkpoints associated to receiving a message (#α ) and spawning a process (#sp ). These checkpoints are internal and only used to ensure causal
consistency.
Also, we now assume that all messages v are transformed into a tuple {t, v}
where t is a unique identifier for this message. Consequently, receive expressions

τ

(Internal )

θ, e → θ′ , e′
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ; hτ (θ, e) : π, p, (θ′ , e′ ), qi&Π
check(y)

(Check )

θ, e → θ′ , e′ and t is fresh
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ; hcheck(θ, e) : #tch : π, p, (θ′ , e′ {y 7→ t}), qi&Π
rec(y,cln )

(Receive)

θ, e → θ′ , e′ matchrec(cln , q) = (θi , ei , q ′ , t)
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ; hrec(θ, e, q) : π, p, (θ′ θi , e′ {y 7→ ei }), q ′ i&Π
send(p′′ ,v)

(Send )

θ, e
→
θ′ , e′ and t is fresh
′′
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ∪ (p, p , {t, v}); hsend(p′′ , θ, e, t) : π, p, (θ′ , e′ ), qi&Π
spawn(y,a/n,[e1 ,...,en ])

(Spawn)

θ, e
→
θ′ , e′ p′ is a fresh pid and t is fresh
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ; hspawn(θ, e, p′ ) : π, p, (θ′ , e′ {y 7→ p′ }), qi
&h[ ], p′ , (θ, (apply a/n (e1 , . . . , en )), [ ]i&Π
self(y)

(Self )

(Sched )

θ, e → θ′ , e′
Γ ; hπ, p, (θ, e), qi&Π ⇀ Γ ; hself(θ, e) : π, p, (θ′ , e′ {y →
7 p}), qi&Π
α(Γ ) = (p′ , p) Π = hπ, p, (θ, e), qi&Π ′
Γ ; Π ⇀ Γ \ (p′ , p, {t, v}); hα(p′ , p, {t, v}) : π, p, (θ, e), {t, v} : qi&Π ′
Fig. 8. Reversible semantics: system rules

should ignore this part of the message when matching with the corresponding
patterns.
Example 3. Consider again the program shown in Figure 6, where the function
client/1 is now defined as follows:
client/1 = fun (S) → let = check in let = S ! {self(), req}
in receive ack → ok end
and the execution trace shown in Figure 7. The corresponding forward (reversible) computation is shown in Figure 9.
4.2

Backward Semantics

Now, we present the backward semantics. The rules can be split into two groups:
the ones required to trigger, manage, and finish a rollback operation, and the
ones that actually perform the backward computation.
We denote a process running backwards with ⌊p⌋Ψ , where Ψ is the set of
pending checkpoints that the backward computation of p has to go through
before resuming its forward computation. For instance, a process of the form
⌊p⌋{#tch } should go backwards until a checkpoint #tch is found in its trace, a
process ⌊p⌋{#tα } should go backwards until an event of the form α(. . . , {t, }) is
found in its trace, and a process ⌊p⌋{#tsp } should go backwards until its initial

⇀
⇀
⇀
⇀

⇀

⇀

⇀

⇀

⇀

[ ]; h[ ], c1, (id, apply main/0 ()), [ ]i
...
[ ]; hπi , c1, (σ, let = check in . . .), [ ]i & hπi′ , s, (id, receive {P, M} → . . .), [ ]i &
hπi′′ , c2, (σ, ok), [ ]i
t

[ ]; hcheck(σ, let = check in . . .) : #ch1 : πi , c1, (σ, let = t1 in . . .), [ ]i &
hπi′ , s, (id, receive {P, M} → . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
t

[ ]; hτ (σ, let = t1 in . . .) : check(σ, let = check in . . .) : #ch1 : πi ,
c1, (σ, let = S ! {c1, req} in . . .), [ ]i &
hπi′ , s, (id, receive {P, M} → . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
[(c1, s, [{t2 , v2 }])]; hsend(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let = t1 in . . .)
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, let = {c1, req} in . . .), [ ]i &
hπi′ , s, (id, receive {P, M} → . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
[(c1, s, [{t2 , v2 }])]; hτ (σ, let = {c1, req} in . . .) : send(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, receive ack → . . .), [ ]i &
hπi′ , s, (id, receive {P, M} → . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
[ ]; hτ (σ, let = {c1, req} in . . .) : send(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, receive ack → . . .), [ ]i &
hα(c1, s, {t2 , v2 }) : πi′ , s, (id, receive {P, M} → . . .), [{t2 , {c1, req}}]i &
hπi′′ , c2, (σ, ok), [ ]i
[ ]; hτ (σ, let = {c1, req} in . . .) : send(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, receive ack → . . .), [ ]i &
hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
...

Fig. 9. A (partial) trace with the forward reversible semantics.

state is reached (i.e., it should be completely undone). Furthermore, a process
may have a set with several pending checkpoints coming from different rollback
operations. Once a checkpoint is reached, it is removed from set Ψ . When Ψ = ∅,
the process p can resume its forward computation (from the last checkpoint).
Let us now explain the rules shown in Figure 10, whose purpose is to mark
(or unmark) a process for backward computation. The first two rules, Undo1
and Undo2 , are used to introduce a new rollback for a checkpoint #tch for some
t.
A backward computation ends when there are no pending checkpoints in the
set (rule Stop1 ) or when we reach a process with an empty trace and a spawn
checkpoint #tsp in the set of pending checkpoints, so that the process is removed
from the system (rule Stop2 ).
Finally, if we reach a checkpoint #tch in the trace of a process running backwards, we can either remove it from the set of pending checkpoints (rule Check )
or just ignore it when it was not in the set of pending checkpoints (rule Discard ).4
Let us now discuss the rules for performing backward computations, which
are shown in Figure 11. In general, these rules are applied whenever the term
located at the top of the computation history π is an event associated to a
sequential or concurrent expression (i.e., when it is not a checkpoint). These
terms are deleted from the trace when any of these rules is applied.
In general, all rules restore the control (and sometimes also the queue) of a
process. In order to reverse the creation of a process, rule Spawn marks the child
4

Note that this may happen often since the evaluation of each function check introduces a checkpoint #tch no matter whether a rollback operation is run or not.

= t1 in . . .)

= t1 in . . .)

= t1 in . . .)

(Undo1 )

Γ ; hπ, p, (θ, e), qi & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋#tch & Π

(Undo2 )

Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ ∪#tch & Π

(Stop1 )

Γ ; ⌊hπ, p, (θ, e), qi⌋∅ & Π ↽ Γ ; hπ, p, (θ, e), qi & Π

(Stop2 )
(Check )

Γ ; ⌊h[ ], p, (θ, e), qi⌋{#tsp } & Π ↽ Γ ; Π
Γ ; ⌊h#tch : π, p, (θ, e), qi⌋Ψ ∪#tch

& Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

(Discard ) Γ ; ⌊h#tch : π, p, (θ, e), qi⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

if #tch 6∈ Ψ

Fig. 10. Backward semantics: rules for dealing with rollbacks
′

process with checkpoint #psp . The child process will then run backwards until,
eventually, its trace is empty and rule Stop2 removes it from the system.
For undoing the sending of a message, rule Send1 removes a message from Γ
when the message has not been delivered yet. Here, we use the operator “\\” to
denote the removal of a message no matter its position (in contrast to “\” which
always removes the oldest message of the list, i.e., the first one). Otherwise, rule
Send2 propagates the backward computation to the receiver process by adding
#tα as a pending checkpoint of the receiver process (t identifies the message).
This will cause the receiver process to undo all the actions that it has performed
since it received the message, thus ensuring causal consistency.
Observe that, at first glance, one may think rule Receive should also introduce
some new rollback operation for causal consistency. However, if we take a closer
look, we will realize that receiving a message in our context is just about processing the message, and not actually receiving it. In fact, the processed message
could have been delivered to the process mailbox a long time ago, and triggering
a backward computation on the sending process would be unnecessary.
It is actually rules Sched1 and Sched2 that take care of dealing with terms of
the form α(p′′ , p, {t, v}) in a trace. When the rollback was introduced by another
process (in rule Send2 ), rule Sched1 removes the corresponding message {t, v}
from the process queue and deletes the checkpoint #tα from the set of pending
checkpoints. No further action is required; actually, when the process p′′ that
triggered rule Send2 resumes its forward computation, the same message v (with
a different identifier t′ ) will be delivered again to process p. When the rollback
was not introduced using rule Send2 , i.e., there is no checkpoint #tα in Ψ , then
Sched2 proceeds as before but also adds the message (p′′ , p, {t, v}) to the global
mailbox Γ . Then, when this process resumes its forward computation, the same
message will again be delivered by the scheduler. Here, the operator ∪ is used
to add messages to the head of the corresponding list instead of to its end, i.e.,
Γ ∪ (p, q, {t, v}) denotes Γ \ {(p, q, vs)} ∪ {(p, q, {t, v} : vs)}.
In both cases, we aim at eventually producing a system that could have been
obtained from the initial state using only forward steps.

Γ ; ⌊hτ (θ, e) : π, p, (θ′ , e′ ), qi⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

(Internal )
(Check )

Γ ; ⌊hcheck(θ, e) : π, p, (θ′ , e′ ), qi⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

(Receive)

Γ ; ⌊hrec(θ, e, q) : π, p, (θ′ , e′ ), q ′ i⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

(Send1 )

Γ ; ⌊hsend(p′′ , θ, e, t) : π, p, (θ′ , e′ ), qi⌋Ψ & Π ↽ Γ ′ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π
if (p, p′′ , {t, v}) occurs in Γ, with Γ ′ = Γ \\(p, p′′ , v, t)

(Send2 )

Γ ; ⌊hsend(p′′ , θ, e, t) : π, p, (θ′ , e′ ), qi⌋Ψ & hπ ′′ , p′′ , (θ′′ , e′′ ), q ′′ i & Π
↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & ⌊hπ ′′ , p′′ , (θ′′ , e′′ ), q ′′ i⌋#tα & Π
if (p, p′′ , {t, v}) does not occur in Γ

(Spawn)

Γ ; ⌊hspawn(θ, e, p′′ ) : π, p, (θ′ , e′ ), qi⌋Ψ & hπ ′′ , p′′ , (θ′′ , e′′ ), q ′′ )i & Π
↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & ⌊hπ ′′ , p′′ , (θ′′ , e′′ ), q ′′ )i⌋#p′′ & Π
sp

(Self )

′

′

Γ ; ⌊hself(θ, e) : π, p, (θ , e ), qi⌋Ψ & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π

(Sched1 ) Γ ; ⌊hα(p′′ , p, {t, v}) : π, p, (θ, e), {t, v} : qi⌋Ψ ∪#tα & Π ↽ Γ ; ⌊hπ, p, (θ, e), qi⌋Ψ & Π
(Sched2 )

Γ ; ⌊hα(p′′ , p, {t, v}) : π, p, (θ, e), {t, v} : qi⌋Ψ & Π
↽ Γ ∪ (p′′ , p, {t, v}); ⌊hπ, p, (θ, e), qi⌋Ψ & Π

if #tα 6∈ Ψ

Fig. 11. Backward semantics: Rules for backward computation.

Example 4. Consider the forward execution trace shown in Figure 9. A corresponding backward computation is shown in Figure 12.
The soundness of our reversible semantics can be stated as follows: i) every
forward step can be reversed; ii) every system reached during a computation
with ⇋, could have been reached with ⇀ from the initial system.

5

Discussion

We have defined a reversible semantics for a first-order subset of Erlang. To the
best of our knowledge, this is the first attempt to define a reversible semantics
for Erlang. As mentioned in the introduction, the closest to our work is the
debugging approach based on a rollback construct of [11, 14–16], but it is defined in the context of a higher-order asynchronous π-calculus. Also, we share
some similarities with the checkpointing technique for fault-tolerant distributed
computing of [9, 12], although the aim is different (they aim at defining a new
language rather than extending an existing one).
As future work, we plan to formally study the correctness of our calculi, as
claimed at the end of the previous section. Also, we would like to extend the
Erlang language with a new construct for safe sessions so that all the actions in
a session can be undone when the session aborts, which has a great potential to
automate the fault-tolerance capabilities of the language Erlang.

[ ]; ⌊hτ (σ, let = {c1, req} in . . .) : send(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, receive ack → . . .), [ ]i⌋ t1 &

= t1 in . . .)

#
ch
hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
′′
s, (θ2 , let = P ! ack in . . .), [ ]i & hπi , c2, (σ, ok), [ ]i

↽ [ ]; ⌊hsend(s, σ, let = S ! {c1, req} in . . . , t2 ) : τ (σ, let = t1 in . . .)
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, let = {c1, req} in . . .), [ ]i⌋

t
# 1
ch

&

hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i
↽ [ ]; ⌊hτ (σ, let = t1 in . . .)
t
: check(σ, let = check in . . .) : #ch1 : πi , c1, (σ, let = S ! {c1, req} in . . . , t2 ), [ ]i⌋

t
# 1
ch

⌊hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i⌋ t2 & hπi′′ , c2, (σ, ok), [ ]i
↽ [ ]; ⌊hcheck(σ, let

t

&

#α

= check in . . .) : #ch1 : πi , c1, (σ, let

= t1 in . . .), [ ]i⌋

t
# 1
ch

&

⌊hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i⌋ t2 & hπi′′ , c2, (σ, ok), [ ]i
t

↽ [ ]; ⌊h#ch1 : πi , c1, (σ, let

#α

= check in . . .), [ ]i⌋

t
# 1
ch

&

⌊hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i⌋ t2 & hπi′′ , c2, (σ, ok), [ ]i
#α

↽ [ ]; ⌊hπi , c1, (σ, let = check in . . .), [ ]i⌋∅ &
⌊hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i⌋#t2 & hπi′′ , c2, (σ, ok), [ ]i
α

↽ [ ]; hπi , c1, (σ, let = check in . . .), [ ]i &
⌊hrec(id, receive {P, M} → . . . , [{t2 , {c1, req}}]) : α(c1, s, {t2 , v2 }) : πi′ ,
s, (θ2 , let = P ! ack in . . .), [ ]i⌋#t2 & hπi′′ , c2, (σ, ok), [ ]i
α

↽ [ ]; hπi , c1, (σ, let = check in . . .), [ ]i &
⌊hα(c1, s, {t2 , v2 }) : πi′ , s, (id, receive {P, M} → . . .), [{t2 , {c1, req}}]i⌋#t2 &

hπi′′ , c2, (σ, ok), [ ]i
↽ [ ]; hπi , c1, (σ, let = check in . . .), [ ]i &
⌊hπi′ , s, (id, receive {P, M} → . . .), [ ]i⌋∅ & hπi′′ , c2, (σ, ok), [ ]i
↽ [ ]; hπi , c1, (σ, let = check in . . .), [ ]i &
hπi′ , s, (id, receive {P, M} → . . .), [ ]i & hπi′′ , c2, (σ, ok), [ ]i

α

Fig. 12. A (partial) trace with the backward reversible semantics.

Acknowledgements
We would like to thank Ivan Lanese and the anonymous reviewers for many
useful suggestions to improve this paper.

References
1. Armstrong, J., Virding, R., Williams, M.: Concurrent programming in Erlang (2nd
edition). Prentice Hall (1996)
2. Bennett, C.: Logical reversibility of computation. IBM Journal of Research and
Development 17, 525–532 (1973)
3. Bennett, C.: Notes on the history of reversible computation. IBM Journal of Research and Development 44(1), 270–278 (2000)
4. Caballero, R., Martı́n-Martı́n, E., Riesco, A., Tamarit, S.: A declarative debugger
for concurrent erlang programs (extended version). Tech. Rep. SIC-15/13, UCM
(2013), http://maude.sip.ucm.es/∼adrian/files/conc cal tr.pdf
5. Cardelli, L., Laneve, C.: Reversible structures. In Proc. of CMSB 2011, pp. 131–
140. ACM (2011)

6. Carlsson, R., Gustavsson, B., Johansson, E. et al : Core erlang 1.0.3. language specification (2004), available from https://www.it.uu.se/research/
group/hipe/cerl/doc/core_erlang-1.0.3.pdf
7. Danos, V., Krivine, J.: Reversible communicating systems. In Proc. of CONCUR
2004. Springer LNCS 3170, pp. 292–307 (2004)
8. Danos, V., Krivine, J.: Transactions in RCCS. In Proc. of CONCUR 2005. Springer
LNCS 3653, pp. 398–412 (2005)
9. Field, J., Varela, C.A.: Transactors: a programming model for maintaining globally
consistent distributed state in unreliable environments. In Proc. of POPL 2005, pp.
195–208. ACM (2005)
10. Frank, M.P.: Introduction to reversible computing: motivation, progress, and challenges. In Proc. of 2nd Conf. on Computing Frontiers, pp. 385–390. ACM (2005)
11. Giachino, E., Lanese, I., Mezzina, C.A.: Causal-consistent reversible debugging. In
Proc. of FASE 2014. Springer LNCS 8411, pp. 370–384 (2014)
12. Kuang, P., Field, J., Varela, C.A.: Fault tolerant distributed computing using asynchronous local checkpointing. In Proc. of AGERE! 2014, pp. 81–93. ACM (2014)
13. Landauer, R.: Irreversibility and heat generation in the computing process. IBM
Journal of Research and Development 5, 183–191 (1961)
14. Lanese, I., Mezzina, C.A., Schmitt, A., Stefani, J.: Controlling reversibility in
higher-order pi. In Proc. CONCUR 2011. Springer LNCS 6901, pp. 297–311 (2011)
15. Lanese, I., Mezzina, C.A., Stefani, J.: Reversibility in the higher-order π-calculus.
Theor. Comput. Sci. 625, 25–84 (2016)
16. Lienhardt, M., Lanese, I., Mezzina, C.A., Stefani, J.: A reversible abstract machine
and its space overhead. In Proc. of the Joint FMOODS 2012 and FORTE 2012
Int’l Conference. Springer LNCS 7273, pp. 1–17 (2012)
17. Matsuda, K., Hu, Z., Nakano, K., Hamana, M., Takeichi, M.: Bidirectionalization
transformation based on automatic derivation of view complement functions. In
Proc. of ICFP 2007, pp. 47–58. ACM (2007)
18. Nishida, N., Palacios, A., Vidal, G.: Reversible term rewriting. In: Kesner, D.,
Pientka, B. (eds.) Proc. of the First International Conference on Formal Structures
for Computation and Deduction (FSCD’16). Leibniz International Proceedings in
Informatics (2016)
19. Phillips, I., Ulidowski, I.: Reversing algebraic process calculi. J. Log. Algebr. Program. 73(1-2), 70–96 (2007)
20. Svensson, H., Fredlund, L.A., Earle, C.B.: A unified semantics for future Erlang.
In Proc. of the 9th ACM SIGPLAN workshop on Erlang, pp. 23–32. ACM (2010)
21. Thomsen, M.K., Axelsen, H.B.: Interpretation and programming of the reversible
functional language RFUN. In Proc. of IFL 2015. Springer (2016), to appear
22. Tiezzi, F., Yoshida, N.: Reversible session-based pi-calculus. J. Log. Algebr. Meth.
Program. 84(5), 684–707 (2015)
23. Yokoyama, T.: Reversible computation and reversible programming languages.
Electronic Notes in Theoretical Computer Science 253(6), 71–81 (2010), proc. of
the Workshop on Reversible Computation (RC 2009)
24. Yokoyama, T., Axelsen, H.B., Glück, R.: Principles of a reversible programming
language. In Proc. of the 5th Conference on Computing Frontiers, pp. 43–54. ACM
(2008)
25. Yokoyama, T., Axelsen, H.B., Glück, R.: Fundamentals of reversible flowchart languages. Theor. Comput. Sci. 611, 87–115 (2016)

