In reversible computing a program can undo a set of past actions. This is useful in many areas including debugging, state-space exploration, and modelling naturally reversible systems. Concurrent reversible programs do not necessarily have a defined most recent action, and therefore rely on cause-respecting reversal,
where an action can be reversed if it has not caused other actions. For this reason analysing the causal relationships between actions in reversible process calculi is important.
One framework used to describe causal relationships is event structures, which are a well-established model of true concurrency. There exist a number of forms of event structures, including prime, asymmetric,
bundle, flow, stable, and general event structures. More recently, reversible forms of some these types of event structure have been defined. We formulate corresponding categories as well as functors and in some cases adjunctions between them. We show that products and coproducts exist in many cases.
CCSK is a reversible variant of CCS, which uses static reversibility, meaning a process retains the same
structure throughout its computation and simply annotates past actions with keys. We use reversible bundle
event structures to define denotational semantics of the reversible process calculus CCSK. CCSK is an uncontrolled reversible calculus, meaning there is no control on whether or when an action reverses and a process can therefore do and undo the same action indefinitely. We therefore modify CCSK to control the
reversibility with a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we exploit event structures' capacity for non-causal reversibility.
The pi-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operational semantics of the pi-calculus have been proposed, which can be classified according to whether transitions are unlabelled (so-called reductions) or
labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows
a process to receive names it already knows from the environment, while the late semantics do not. All
existing reversible versions of the 휋-calculus use reduction or late semantics, despite the early semantics
of the (forward-only) 휋-calculus being more widely used than the late. We de ne 휋IH and 휋IK, the rst
reversible early 휋-calculi. The new calculi are a reversible form of the internal 휋-calculus, which is a subset
of the 휋-calculus where every link sent by an output is private, yielding greater symmetry between inputs
and outputs. We also de ne denotational event structure semantics of 휋IK and operational event structure
semantics of 휋IH and prove an equivalence between the two.