On the Expressiveness of Asynchronous Processes with Nested Session Types

On the Expressiveness of Asynchronous Processes with Nested Session Types Sjors Wortelboer

Dan Frumin

Jorge A. Pérez

arXiv:2610.32558v1 [cs.PL] 23 Oct 2026

University of Groningen, The Netherlands

Session types are a type-based approach to correct message-passing programs, where types specify protocols for channels and type checking guarantees communication correctness. Traditional session types express regular protocols only, which leaves out many protocols found in practice. Aiming at overcoming this limitation, Nested Session Types (NSTs) can specify nested recursive protocols. NSTs are known to be characterised by one-counter machines and deterministic context-free languages. In this paper, we study the expressiveness of ASP (Asynchronous Session Processes), the process model associated with NSTs as introduced by Das et al.. We prove that ASP is Turing complete by giving a correct encoding of two-counter machines into typed processes. Our encoding uses a non-trivial state-aware representation of counters and instructions that is neatly governed by NSTs.

1

Introduction

Ensuring the correctness of the message-passing programs that underpin large-scale distributed systems is a fascinating and pressing challenge. We are interested in compositional approaches to program verification where types specify protocols for channels and type checking statically guarantees communication correctness for implementations, specified as processes in some suitable formalism. In this approach, expressiveness is a primary concern, in two ways: first, we aim for rich type systems that can express communication structures found in real-world scenarios; second, since types soundly enforce correctness by constraining admissible program behaviours, we would like to determine the expressiveness of the resulting typed processes—which correct programs can be expressed in a typed setting and which cannot. In this paper, we study the expressiveness of a process language with Nested Session Types (NSTs) by Das et al. [9, 10]. NSTs are among the most expressive type systems for concurrency proposed to date. Session types specify the order and type of messages to be exchanged on a channel [12, 13]. Traditional session types can express regular protocols, as a communication action and a continuation protocol can be composed. However, many practical protocols are not regular; examples include protocols for the (de)serialisation of tree-structured data [22] and for (buffered) message relaying [14]. The quest for more expressive session types led to the context-free session types by Thiemann and Vasconcelos [22]. In context-free session types, generalised protocol composition combined with polymorphic recursion enables the specification of context-free protocols. NSTs achieve high expressivity using different means, namely nested type constructors, which allow recursive type parameters to act like a stack. A crucial step in laying the foundations of non-regular session types is studying what we may refer to as their intrinsic expressiveness: the properties of these infinite structures in themselves, independent of a target programming model. Important notions for verification (type duality, type equality, subtyping) concern types in isolation. In this respect, the theory of context-free session types is well-developed [1, 2, 21]; for NSTs, Das et al. prove that type equality is decidable and give a sound algorithm. Gay et al. [11] offer a unified treatment of intrinsic expressiveness results for recursive session types. They complement the results in [9, 10] and obtain a strict hierarchy where NSTs are precisely characterised by one-counter machines and deterministic context-free languages, with decidable type equivalence and duality. Preliminary Report. Final version to appear in: EXPRESS/SOS 2026

© S. Wortelboer, D. Frumin & J.A. Pérez This work is licensed under the Creative Commons Attribution License.

2

On the Expressiveness of Asynchronous Processes with Nested Session Types

In this paper, we pursue a different yet complementary goal: establishing the expressiveness of the language underlying NSTs, as introduced by Das et al. [9, 10]. We refer to this language as ASP (Asynchronous Session Processes). The language implements asynchronous communication in configurations, which contain processes; its formulation follows the Curry-Howard correspondence between intuitionistic linear logic and session types [8]. As a result, well-typed configurations in ASP enjoy confluence and deadlock freedom. However, the question of the expressiveness of well-typed ASP configurations remains open. Given the context-free nature of NSTs and the decidability of their key properties, we investigate whether the synchronisation mechanisms in ASP, together with the intrinsic expressiveness of types, suffice to obtain Turing completeness. Our main result answers this question affirmatively. We prove that ASP is Turing complete by correctly encoding Minsky machines [19]. Minsky machines are a Turing-complete model that consists of two counters with a finite set of instructions; instructions can either increment a counter, decrement it (if the counter’s current value is not zero), or jump to a given instruction (if the value is zero). With this minimal state and set of possible instructions, Minsky machines are, arguably, a simpler source for encoding, compared to Turing machines. Let us briefly discuss how we model Minsky machines in ASP. Intuitively, counters can be implemented as stacks using polymorphic nested types to capture state at the type level. Given a natural m, we define the nested type ( 0[] if m = 0 LmM = S[Lm − 1M] if m > 0 where 0 and S stand for (parametric) type definitions for zero and successor, given as follows: 0[] ≜ &{incr : S[0[]], jump : 0[]}

S[α] ≜ &{incr : S[S[α]], decr : α}

Expressed as a branching type (&, external choice), this nested session type captures the protocol that specifies the correct state after executing an instruction, using nested types and polymorphic recursion. This way, e.g., 0[] admits increment and jump (but not decrement) and S[α] admits increment and decrement (but not jump) by suitably modifying the nesting of the type variable α, the parameter of S. Such counter types can then be combined on the process level (by a process that we will denote JmKr ) with the consequence that processes representing instructions are required to be state-aware: they need a separate mechanism to keep track of the combined state of the two counters. This is where NSTs enable a continuation of the state-aware processes, allowing transitions to be captured at the level of processes. Overall, we believe that our encoding of Minsky machines is a significant test of the expressiveness of the coupling of ASP and NSTs. Indeed, we achieve a pleasant design in which NSTs elegantly govern the correct behaviours of the encodings of counters and instructions, and their interactions. The rest of the paper is structured as follows. Section 2 recalls background notions of ASP and NSTs and the definition of Minsky machines. The encoding of Minsky machines in ASP is presented and illustrated in Section 3; its correctness is given in terms of typability (Theorem 4) and operational correspondence (Theorems 5 and 6). Section 4 concludes the paper and discusses some related work.

2

Background

2.1

Nested Session Types

We first present Nested Session Types (NSTs), then their associated process language, which we call Asynchronous Session Processes (ASP), and finally we state the correctness properties ensured by typing.

S. Wortelboer, D. Frumin & J.A. Pérez

3

Nested Session Types NSTs extend the Curry-Howard correspondence between session types and intuitionistic linear logic [8] with type variables and type definitions. There is a finite signature Σ that collects these type definitions. The syntax and operational interpretation of types is given next. Definition 1 (Nested Session Types, NSTs). The language of nested session types (NSTs) is defined by: A, B,C ::= A ⊗ B

send channel of type A, continue as B

|A⊸B

receive channel of type A, continue as B

| ⊕ {l : Al }l∈L

send label k ∈ L, continue as Ak

| &{l : Al }l∈L

receive label k ∈ L, continue as Ak

|1

close channel

|α

type variable

| V [θ ]

defined type name (in Σ)

Type variables (denoted α, β , . . .) enable the parametrisation of types. NSTs do not make use of type variable binders; instead, type definitions act as binders for a sequence of type variables by which they are parameterised. Type names are defined according to a type definition, denoted V [α] ≜ A, where α is a list of distinct variables A can refer to. These definitions are stored in the signature Σ and allow nested type construction. The type V [θ ] denotes the instantiation of a type name V , which equirecursively unfolds into A with type parameters substituted using θ = A/α. Any type that is not a type name is structural (e.g. V1 [θ 1 ] ⊗ V2 [θ 2 ]). Any type that is structural and not a type variable is contractive in the type definitions. Types without free type variables are called closed types. A key result in [10] is that type equality is decidable and has a sound algorithm. Type equality follows the judgment ψ; V ⊢Σ A ≡ A′ where V denotes the free variables in A and A′ , and ψ is a collection of closures of the form V [θ ] ≡ U[σ ] used to terminate cyclic equivalences. The Process Language We now introduce the process language ASP. This is exactly the language introduced by Das et al. [9, 10]. It is based on the intuitionistic variant of the Curry-Howard correspondence, under an asynchronous communication discipline. Definition 2 (Processes and Messages). Given a set of channel/names ranged over by x, y, z, . . ., the syntax of processes and is defined by: send channel y over x

| y ← recv x; P

| x.li ; P

send label li over x

| case x (li ⇒ Qi )li ∈L

receive a label over x

| close x

closed channel x

| wait x; P

wait for closing of x

P, Q ::= send x y; P

| x ← f [θ ] y; P process name f [] in Σ

receive a channel over x

|x↔y

forward x along y

The syntax of messages is defined by: M ::= send x y; x ↔ x′ | x.k; x ↔ x′ | close x The syntax of processes follows the syntax of types closely. Notable is the addition of process definitions f [θ ] as a dual of nested type construction on the type level. A definition is instantiated, providing channel x to the continuation process P and making use of channels y. Process definitions, similar to type definitions, are defined on the global signature Σ. Messages co-exist with processes as atomic processes to enable asynchronous message passing. They lift sending actions from their processes such that they can be consumed by their dual. Messages preserve linearity by renaming their channel continuation, which matches the continuation of the process producing them.

4

On the Expressiveness of Asynchronous Processes with Nested Session Types

V; ∆, y : A ⊢ P :: (x : B) ⊸R V; ∆ ⊢ y ← recv x; P :: (x : A ⊸ B)

·; V ⊢ A ≡ A′ V; ∆, x : B ⊢ Q :: (z : C) ⊸L ′ V; ∆, x : A ⊸ B, y : A ⊢ send x y; Q :: (z : C)

(∀l ∈ L) V; ∆ ⊢ Pl :: (x : Al ) &R V; ∆ ⊢ case x (l ⇒ Pl )l∈L :: (x : &{l ⇒ Al }l∈L ) (k ∈ L) V; ∆ ⊢ Q :: (x : Ak ) &L V; ∆, x : &{l ⇒ Al }l∈L ⊢ x.k; Q :: (z : C) y′ : B′ ⊢ f [α] = Pf :: (x′ : B) ∈ Σ ·; V ⊢ ∆′ ≡ y : B′ [θ ] V; ∆, x : B[θ ] ⊢ Q :: (z : C) def ′ V; ∆, ∆ ⊢ x ← f [θ ] y; Q :: (z : C) Figure 1: Selected typing rules for ASP (Definition 3). Definition 3 (Typing for Processes & Messages). Given an environment of type variables V, the typing judgment for processes and messages is denoted V; ∆ ⊢Σ P :: (x : A), with selected typing rules in Figure 1 (Appendix A.1 gives a full account). Following the intuitionistic (two-sided) presentation of linear logic, duality is defined implicitly, where a type is provided by the process over the intuitionistic channel and used by a client process over a channel in their environment. As a consequence, there are two typing rules per typing connective. We discuss the rules. Receiving (⊸) is implemented by the providing process by adding the channel y to the continuation. The dual sending action by the client process removes the channel y to preserve linearity. Furthermore, it relies on type equality on the type of channel y, such that the receiving process can use a structurally different but equivalent type. Offering a choice (&{·}) is implemented as branching on the providing process, where the client process selects the branch. Process definitions (def) require a well-typed definition from Σ. All types use the substitution θ where, similar to sending, dependent channels are matched using type equality to allow for better compatibility when composing processes. Finally, the continuation process simply matches the substituted type provided by the definition. The operational semantics of the language is defined in terms of configurations, given next. Definition 4 (Configurations: Syntax and Typing). The syntax of configurations is defined by: S ::= proc(x, P) | msg(x, M) | (S1 , S2 )x The typing rules are as follows: ·; ∆ ⊢ P :: (x : A) proc ∆ |=Σ proc(x, P) :: (x : A)

·; ∆ ⊢ M :: (x : A) msg ∆ |=Σ msg(x, M) :: (x : A)

∆1 |=Σ S1 :: (x : A) x : A, ∆2 |=Σ S2 :: (y : B) comp ∆1 , ∆2 |=Σ (S1 , S2 )x :: (y : B) Configurations lift processes and messages with only closed types to the configuration level, as protocols need to be fully executable. The typing rule for composition binds a channel provided by some configuration S1 to some configuration S2 that uses it. This is the classical rule for composition derived

S. Wortelboer, D. Frumin & J.A. Pérez

proc(y, send x w; P) −→ msg(x, send x w; x ↔ x′ ), proc(y, P[x′ /x])

5

(⊸ S)

proc(x, w′ ← recv x; Q), msg(x, send x w; x ↔ x′ ) −→ proc(x′ , Q[x′ /x, w/w′ ]) proc(d, x.k; P) −→ msg(x, x.k; x ↔ x′ ), proc(d, P[x′ /x])

(⊸ C) (&S)

proc(x, case x (l ⇒ Ql )), msg(x, x.k; x ↔ x′ ) −→ proc(x′ , Qk [x′ /x]) proc(z, x ← f [θ ] d; Q) −→ proc(a, Pf [a/x, d/y, θ ]), proc(z, Q[a/x])

(&C) (defC)

Figure 2: Selected reduction rules for ASP (Definition 5). from linear logic; it defines a partial ordering of the components of the configuration, and any configuration that has the same partial ordering is equivalent. We omit this presentation of composition as the bindings in the encoding are clearly defined. We may now define reduction on the level of configurations. Definition 5 (Reductions). The reduction semantics for configurations is denoted −→, with selected rules in Figure 2 (see Appendix A.2 for details). The rules in Figure 2 illustrate the asynchronous nature of communication in ASP. Sending actions reduce independently by producing a message; a corresponding receiving action consumes the produced message separately. Consequently, a send action does not have to wait for the message to be consumed, and the receiving action does not have to be ready. Messages are produced to the right if sent over the intuitionistic channel and to the left otherwise, with renaming of channels to ensure the correct order of consumption. This preserves linearity and ensures type preservation. Similarly, process definitions produce a newly spawned process to the left of the continuation. Whenever the continuation Q is omitted, forwarding is implied as a continuation of the current process, skipping the renaming. Properties of Typed Configurations We state here some properties of well-typed configurations. First, protocols are invariant under reduction. Theorem 1 (Type preservation). For a well-typed configuration in ∆ |=Σ S :: (x : A): 1. If S ≡ S ′ , then ∆ |=Σ S ′ :: (x : A); 2. If S −→ S ′ , then ∆ |=Σ S ′ :: (x : A). Due to the acyclic nature of composition in ASP, inherited from linear logic, progress is guaranteed for internal channels. A process ready to receive, or a message over an external channel, is called poised; configurations consisting of only poised components are also called poised. Theorem 2 (Progress). Suppose ∆ |=Σ S :: (x : A). Either S is poised, or S −→ S ′ . Finally, confluence emerges due to the sequential independent definitions of reductions. The language supports deterministic choices only, and so reductions persist until consumed—they can always be applied, creating different orders of application with the same resulting process. Theorem 3 (Confluence). Suppose a configuration S in ASP. If S −→∗ S1 and S −→∗ S2 , then there exists S ′ such that S1 −→∗ S ′ and S2 −→∗ S ′ .

6

On the Expressiveness of Asynchronous Processes with Nested Session Types State (Definition 13)

Counters (Definition 10)

J(i, m0 , m1 )KM ≜ Jm0 Kr0 , Jm1 Kr1 , {|m0 , m1 |}tM , Ji | m0 , m1 KM r0 ,r1 ,t Instantiation process (Definition 12) Instruction process (Definition 11)

Figure 3: Roadmap to the encoding of Minsky machine state in ASP.

2.2

Minsky machines

To show Turing-completeness for ASP we need an appropriate formalism. We consider Minsky machines, which have a simpler structure than Turing machines. Minsky machines are Turing-complete, and so any system able to simulate them is by extension Turing-complete. In the following, we often use ‘machine’ as shorthand for ‘Minsky machine’. Definition 6 (Minsky machines [19]). A Minsky machine M is defined as a set of instructions {(1 : I1 ), ...., (n : In )}, where instructions are defined as: increment on counter j ∈ {0, 1}

I ::= INC( j)

decrement or jump on counter j ∈ {0, 1}, k ∈ Z+

| DECJ( j, k)

A machine includes a program counter p indicating the label of the instruction being executed. The machine starts with both counters set to 0 and the program counter p set to the first instruction. The machine stops whenever the program counter is set to a non-existent instruction, i.e., p > n. The state of a machine M is defined as the tuple (i, m0 , m1 )M , where i ∈ Z+ and m0 , m1 ∈ N. The tuple refers to the current instruction i and the counters with values m0 and m1 . The state is initialised to zero values on the counters and instruction i as associated with the machine M. The semantics of the machine is defined as a relation on states, denoted −→M , given next: i : INC( j)

m′j = m j + 1

m′1− j = m1− j

(i, m0 , m1 )M −→M (i + 1, m′0 , m′1 )M i : DECJ( j, k)

mj > 0

m′j = m j − 1

m′1− j = m1− j

(i, m0 , m1 )M −→M (i + 1, m′0 , m′1 )M mj = 0 M (i, m0 , m1 ) −→M (k, m0 , m1 )M i : DECJ( j, k)

Incr

Decr

Jump

The instructions can only manipulate the state. In case of a successful instruction i (increment or decrement), the appropriate counter is updated, and the machine moves to the next instruction i + 1. Decrementing is only possible when the counter value is not zero; otherwise, the value remains unchanged, and the machine jumps to instruction k.

S. Wortelboer, D. Frumin & J.A. Pérez

3

7

Encoding Minsky Machines in ASP

In this section, we show how to encode the state of a machine M into ASP. The encoding shows that ASP is Turing complete, and illustrates how NSTs can express stateful types that govern the behaviour of the encoding at the process level. The starting point for our proposed encoding is LmM, the interaction protocol for the representation of the natural number m, discussed in the introduction. Given a machine M with state (i, m0 , m1 ), we define a configuration in ASP denoted J(i, m0 , m1 )KM . As Figure 3 shows, we consider encodings of the counters, an instruction process that is state-aware (i.e., it depends on the state of the counters), as well as an instantiation process. As we will see, the encoding of counters by itself is not sufficient to accurately determine the next instruction, in particular when performing decrements; to address this, the instantiation process codifies sufficient information about M to correctly enable the next instruction. The correctness of our encoding follows from • the typability of J(i, m0 , m1 )KM (Theorem 4) and

• operational correspondence results, which ensure that (i) every step possible from (i, m0 , m1 ) is correctly mimicked by J(i, m0 , m1 )KM (soundness, Theorem 5) and (ii) all steps arising from J(i, m0 , m1 )KM correspond to steps enabled from (i, m0 , m1 ) (completeness, Theorem 6). We first describe the stateful representation at the level of types, namely the one-counter types that capture the state of the counters (Definition 7), and the instruction instantiation type, which enables the continuation of instructions when decrementing (Definition 9). These types provide the appropriate interfaces for typing the processesin Figure 3: counters Jmi Kri (with i ∈ {0, 1}), the instantiation process {|m0 , m1 |}tM , and the encoding of the instruction Ji | m0 , m1 KM r0 ,r1 ,t . These interfaces, in turn, are crucial to enable the safe composition required to obtain the configuration J(i, m0 , m1 )KM given by Definition 13. Given a machine M, we will define an associated signature ΣM . In giving the different ingredients of the encoding, we will be presenting type and process definitions that we assume are present in ΣM . Types and processes for the encoding are presented in Section 3.1 and Section 3.2, respectively. The correctness of the encoding is established in Section 3.3, whereas an example illustrating the role of the different components of the encoding is given in Section 3.4.

3.1

Stateful Protocols

As already discussed, a key idea in our encoding is using Peano’s representation of the naturals as a protocol that relies on nesting of type parameters in NSTs. We will have two protocols, one per counter, and so the challenge lies in coordinating their behaviour according to the instructions of the machine. Definition 7 (Stateful counter protocol). Given a natural number m, its associated counter type is: ( 0[] if m = 0 LmM = S[Lm − 1M] if m > 0

(1)

with type definitions in ΣM : 0[] = &{incr : S[0[]], jump : 0[]}

(zero)

S[α] = &{incr : S[S[α]], decr : α}

(successor)

This protocol is self-explanatory: the choices incr, jump, and decr correspond to the three possible reduction steps for a machine (increments, decrements, jumps), while accounting for successive steps.

8

On the Expressiveness of Asynchronous Processes with Nested Session Types

This is preferable to having two labels corresponding to instructions (with sub-cases for decrement-andjump). The nesting in types is evident, as is the fact that state does not change in the case of a jump. As a convention, we use type variables α and β as parameters for the first and second counter, respectively. In principle, given an instruction i of M, we would like to have an encoding of instructions JiKM r0 ,r1 with judgement ·; r0 : Lm0 M, r1 : Lm1 M, · · · ⊢ JiKM r0 ,r1 :: (x : 1)

where r0 , r1 are names where the protocol counters are implemented. Clearly, we do not know the exact type of instruction i, whether it operates on r0 or r1 , or whether it may result in a jump. Our encoding of instructions must then be state-aware. As such we define a process Ji | m0 , m1 KM r0 ,r1 , which depends on either 0[] or S[α] on r0 and r1 . An issue then arises: the protocol becomes α in case of a decrement, which is insufficient to capture the state of the counter. Indeed, without extra information, the next instruction cannot be instantiated for the decrementing case, as it depends on 0[] or S[·]. To overcome this difficulty, the instantiation process will act as a coordinator between the process representation of counters and instructions. We define a corresponding instantiation protocol for instructions, able to match α after decrementing a counter as well as to trigger the next instruction, enabling interaction with both counters. To define the instantiation protocol, we first characterise all the instructions that may occur in the possible states of M; this is needed to define ΣM appropriately. We use the following auxiliary notion. Definition 8. Given a machine M, the set of accessible instructions LM is defined as LM = {i + 1 | (i : Ii ) ∈ M} ∪ {k | (i : DECJ( j, k)) ∈ M} The set LM contains indices for the instructions of M and possible indices that lie out of bounds of M. It is not the set of all the reachable instructions, but an over-approximation of it. It is easy to verify that the set LM is finite, as there are only finite instructions in M. Definition 9 (Instantiation protocol). Given m0 , m1 ∈ N and a machine M, the instantiation protocol T M Lm0 , m1 M is given as:   T 0,0 [] if m0 = m1 = 0    T s,0 [Lm − 1M] if m0 > 0 ∧ m1 = 0 0 T M Lm0 , m1 M = (2) 0,s T [Lm1 − 1M] if m0 = 0 ∧ m1 > 0    T s,s [Lm − 1M, Lm − 1M] if m > 0 ∧ m > 0 0 1 0 1 with the type definitions in Figure 4 included in ΣM . In this definition, the superscript in T −,− denotes the reflection of the zero/successor state of the onecounter types. This agnostic protocol enables the handoff of the one-counter channels to some process abstracting the transition to jump at the process level. The choices that are associated with incrementing and decrementing are called expansion (exp) and instantiation (ins), respectively. Expansion predicts the next state, while instantiation simply receives the dependencies of the current instruction and the next instruction. The choices for duplication (dup) and termination (ter) are for bookkeeping purposes related to the decrementing tree data structure process that the protocol is implemented in.

3.2

Processes

Having presented the nested session types that govern our encoding, we turn our attention to processes. We first give the encoding of the counter process, which closely follows the one-counter protocol; it is a dependency of the instruction process.

S. Wortelboer, D. Frumin & J.A. Pérez

9

T 0,0 [] = &{ exp0 : T s,0 [0[]], dup : T 0,0 [] ⊗ T 0,0 [], T

s,0

exp1 : T 0,s [0[]], ter : 1

}

[α] = &{ ins0 : I[α, 0[]], exp0 : T s,0 [S[α]],

exp1 : T s,s [α, 0[]],

dup : T s,0 [α] ⊗ T s,0 [α],ter : 1

}

T 0,s [β ] = &{ ins1 : I[0[], β ], exp0 : T s,s [0[], β ], β ], exp1 : T 0,s [S[β ]], dup : T 0,s [β ] ⊗ T 0,s [β ],ter : 1 s,s

T [α, β ] = &{ ins0 : I[α, S[β ]], s,s

}

ins1 : I[S[α], β ],

exp0 : T [S[α], β ],

exp1 : T s,s [α, S[β ]],

ter : 1

}

I[α, β ] = α ⊸ β ⊸ 1 ⊸ &{i : 1}i∈LM Figure 4: Type definitions for the instantiation-protocol (Definition 9). Definition 10 (Encoding a counter). The encoding of a counter containing m ∈ N into a configuration S in ASP is given as follows, using Definition 7: ( proc(r, R0 ) if m = 0 JmKr = (3) s Jm − 1K p , proc(r, R [Lm − 1M/α]) if m > 0 with process definitions in ΣM :

· ⊢ r0 [] = R0 :: (r : 0[])

p : α ⊢ rs [α] = Rs :: (r : S[α])

and the constituent process definitions: R0 = case r (incr ⇒ c ← r0 []; r ← rs [0[]] c, jump ⇒ r ← r0 [] )

Rs = case r (incr ⇒ c ← rs [α] p; r ← rs [S[α]] c, decr ⇒ p ↔ r )

As mentioned before, while Jm0 Kr0 uses type variable α, the definition of Jm1 Kr1 uses β . Each counter is implemented as a stack, following the protocol definition. The continuation process for each choice reflects the construction of the continuation type. For increments, this is the re-instantiation of the current process followed by the successor. For jumps, we only re-instantiate the zero counter process. For decrements, the process providing α is forwarded. The encoding of instructions is state-aware and meant to interact with the instantiation process: Definition 11 (Instruction processes). Given some instruction i ∈ Z+ of M, the encoding of i into a configuration S in ASP depends on the values of the counters m0 , m1 ∈ N; it is given as follows, using Definitions 7 and 9:   proc(x, Pi0,0 ) if m0 = m1 = 0    proc(x, Ps,0 [Lm − 1M/α]) if m0 > 0 ∧ m1 = 0 0 i Ji | m0 , m1 KM r0 ,r1 ,t =  0,s proc(x, Pi [Lm1 − 1M/β ]) if m0 = 0 ∧ m1 > 0    proc(x, Ps,s [Lm − 1M/α, Lm − 1M/β ]) if m > 0 ∧ m > 0 0 1 0 1 i

10

On the Expressiveness of Asynchronous Processes with Nested Session Types

  r0 .incr; t.exp0 ; x ← ps,0  i+1 [0[]] r0 r1 t y   r .incr; t.exp ; x ← p0,s [0[]] r r t y 1 1 0 1 i+1 Pi0,0 = 0,0  r .jump; x ← p [] r r t y j 0 1  k   wait y; Q0,0 i   r0 .incr; t.exp0 ; x ← ps,0  i+1 [S[α]] r0 r1 t y   s,s   r1 .incr; t.exp1 ; x ← pi+1 [α, 0[]] r0 r1 t y s,0 Pi = r0 .decr; t.ins0 ; send t r0 ; send t r1 ; send t y;t.(i + 1); t ↔ x    r1 .jump; x ← ps,0   k [α] r0 r1 t y   s,0 wait y; Qi   r0 .incr; t.exp0 ; x ← ps,s  i+1 [0[], β ] r0 r1 t y   0,s   r1 .incr; t.exp1 ; x ← pi+1 [S[β ]] r0 r1 t y Pi0,s = r0 .jump; x ← p0,s k [β ] r0 r1 t y    r1 .decr; t.ins1 ; send t r0 ; send t r1 ; send t y;t.(i + 1); t ↔ x     wait y; Q0,s i   r0 .incr; t.exp0 ; x ← ps,s  i+1 [S[α], β ] r0 r1 t y   r .incr; t.exp ; x ← ps,s [α, S[β ]] r r t y 1 1 0 1 i+1 Pis,s =  r .decr; t.ins ; send t r ; send t r j j 0 1 ; send t y;t.(i + 1); t ↔ x    wait y; Qs,s i

if i : INC(0) if i : INC(1) if i : DECJ( j, k) if i > n if i : INC(0) if i : INC(1) if i : DECJ(0, k) if i : DECJ(1, k) if i > n if i : INC(0) if i : INC(1) if i : DECJ(0, k) if i : DECJ(1, k) if i > n if i : INC(0) if i : INC(1) if i : DECJ( j, k) if i > n

Figure 5: Constituent processes used in the encoding of instructions (Definition 11). with the process definitions in ΣM using Definition 8: r0 : 0[], r1 : 0[], t : T 0,0 [],

y : 1 ⊢ p0,0 i∈LM []

= Pi0,0 :: (x : 1)

r0 : S[α], r1 : 0[], t : T s,0 [α],

y : 1 ⊢ ps,0 i∈LM [α]

= Pis,0 :: (x : 1)

r0 : 0[], r1 : S[β ], t : T 0,s [β ],

y : 1 ⊢ p0,s i∈LM [β ]

= Pi0,s :: (x : 1)

s,s r0 : S[α], r1 : S[β ], t : T s,s [α, β ], y : 1 ⊢ ps,s i∈LM [α, β ] = Pi :: (x : 1)

and the constituent process definitions are given in Figure 5. In this definition, the subscripts r0 , r1 , and t in the encoding refer to the internal renaming of the channels of the counter processes 0 and 1 and the instantiation process, in that order. Channels x and y never reduce; hence, no renaming is necessary. Note that x is merely an artefact of the intuitionistic nature of the calculus and needs to be included. The definitions for the instruction processes deal with branching by being state-aware, which is a consequence of the stateful protocols; an instruction must know when it can decrement or when it should jump, and deal with the subsequent state accordingly. This highlights the need for the instantiation protocol/process: without it, the instruction cannot move forward. In Figure 5, the instructions are implemented by sending the appropriate label associated with the current instruction action over the corresponding counter channel. For incrementing and jumping, it is

S. Wortelboer, D. Frumin & J.A. Pérez

11

possible to predict the next state; hence, we can instantiate the next instruction directly; for example, in the encoding of increments as defined in Pi0,0 . Note that for increments the state of the counters is synchronised with the instantiation process; this is not necessary for jumps, as the state remains unchanged. The case for decrementing is slightly different after sending the label, as it is impossible to instantiate the next instruction over a generic type variable. Instead, the current instruction hands off the dependent processes and the next instruction index to the instantiation process, which closes the circle and allows the definitions to be well-typed; this occurs, for example, in the encoding of decrement-jump in Pis,s . Lastly, there is a special case for out-of-bounds instructions. In this case, the machine cannot reduce further and has terminated. To simulate this, we use the external channel y, which halts further progress; for example, in the encoding of out-of-bound i in Pi0,0 . The continuation process Qi can be any process as long as it is distinct for different i, to capture the final state for each possible value of i. Similar to Definition 10, process definitions are added to the global environment ΣM to move to instructions and make use of LM (Definition 8) to include the finite set of accessible instructions. Unlike the process definitions, which are defined on LM , the encoding of an instruction is unbounded. To continue to the next instruction after decrementing, we rely on the instantiation process, defined next. The definitions make use of a decrementing tree data structure, as it is the most straightforward both in implementation and in understanding the bookkeeping involved. Definition 12 (Instantiation process). Given some m0 , m1 ∈ N, the instantiation process {|m0 , m1 |}tM is a configuration S in ASP defined as follows, using Definitions 7, 9 and 11:  proc(z, N 0,0 ) if m0 = m1 = 0     M 1,0   {|0, 0|}a , proc(z, N ) if m0 = 1 ∧ m1 = 0    M s,0   {|m − 1, 0|}a , proc(z, N [Lm0 − 2M/α]) if m0 > 1 ∧ m1 = 0     M 0,1  {|0, 0|}b , proc(z, N ) if m0 = 0 ∧ m1 = 1     0,s {|0, m1 − 1|}M if m0 = 0 ∧ m1 > 1 b , proc(z, N [Lm1 − 2M/β ]) {|m0 , m1 |}M (4) z = M M 1,1  {|0, 1|}a , {|1, 0|}b , proc(z, N ) if m0 = m1 = 1     M s,1  {|m0 − 1, 1|}M  a , {|m0 , 0|}b , proc(z, N [Lm0 − 2M]/α]) if m0 > 1 ∧ m1 = 1    M 1,s  {|0, m1 |}M if m0 = 1 ∧ m1 > 1  a , {|1, m1 − 1|}b , proc(z, N [Lm1 − 2M/β ])    M M {|m0 − 1, m1 |} , {|m0 , m1 − 1|} , if m0 > 1 ∧ m1 > 1  a b    proc(z, N s,s [Lm0 − 2M/α, Lm1 − 2M/β ]) with the process definitions in ΣM : ·; ·

⊢ t 0,0 []

= N 0,0 :: (z : T 0,0 [])

·; a : T 0,0 []

⊢ t 1,0 []

= N 1,0 :: (z : T s,0 [0[]])

α; a : T s,0 [α]

⊢ t s,0 [α]

= N s,0 :: (z : T s,0 [S[α]])

·;

b : T 0,0 []

⊢ t 0,1 []

= N 0,1 :: (z : T 0,s [0[]])

β;

b : T 0,s [β ]

⊢ t 0,s [β ]

= N 0,s :: (z : T 0,s [S[β ]])

·; a : T 0,s [0[]],

b : T s,0 [0[]]

⊢ t 1,1

= N 1,1 :: (z : T s,s [0[], 0[]])

⊢ t s,1 [α]

= N s,1 :: (z : T s,s [S[α], 0[]])

b : T s,s [0[], S[β ]] ⊢ t 1,s [β ]

= N 1,s :: (z : T s,s [0[], S[β ]])

α; a : T s,s [α, 0[]], b : T s,0 [S[α]] β ; a : T 0,s [β ],

α, β ; a : T s,s [α, S[β ]], b : T s,s [S[α], β ] ⊢ t s,s [α, β ] = N s,s :: (z : T s,s [S[α], S[β ]])

12

On the Expressiveness of Asynchronous Processes with Nested Session Types

N 0,0 0

1

N 1,0 0

N 0,1 0

1

N s,0

1 N 0,s

N 1,1 1

0

0

1 N 1,s

N s,1

0

0

1 0

1

N s,s

0,1

1

Figure 6: Instantiation process (Definition 12): Dependencies between constituent process definitions indicating decrements over either the first (0) or the second (1) counter. Figure 7 gives selected cases of the constituent processes definitions; Figure 6 presents a dependency graph. A full account is given in Appendix B.1. The instantiation process {|m0 , m1 |}tM implements a tree-like structure where processes N −,− represent nodes. The encoding builds naturally on the one-counter protocols, creating dependencies on states of decrements on the counters forming the tree structure, where the channels a and b denote whether the first or second counter is decremented, respectively. The dependencies of the composition are presented in Figure 6. Here, the superscript notation of Definition 9 is reused with the addition of 1. In the context of the protocol, this annotation was used merely to denote state; in this definition, it is expanded to reflect the transitions between states. • 0 refers to a zero state without transition; • 1 refers to the transition from a successor to a zero state; • s refers to the transition from a successor to a successor state. Transitions are thus implemented as a dependency on a type definition, unlike the counter, which uses a generic type parameter for its dependency. Consequently, these processes are instantiated using the second-order predecessor, where counters and instructions depend on the first-order predecessor. In Figure 7 we present the most representative constituent process nodes of the instantiation process, with the remaining nodes following similar constructions. We can differentiate nodes by the number of decrementing dependencies in the tree: leaf nodes where both counters are zero, linear nodes with one non-zero counter and binary nodes with both counters non-zero. We comment on some of them: • Node N 0,0 is a leaf that just captures the zero state for both counters. This node exists primarily due to the infinite recursive nature of the one-counters and forms the starting point from which the decrementing tree is constructed, both in the encoding and in the simulation. • Node N 1,0 is a linear node that captures the state of 1 for the first counter and the transition to 0. All states are constant, and therefore, it uses only closed types. The non-zero state implements instantiation to enable progress after decrement, which simply carries over the dependencies of the previous instruction, followed by the instantiation of the next instruction as designated by the current instruction. In case of an increment on the zero state, the node becomes binary by creating a new branch, creating a duplicate to create the choices. Because the node represents a zero state

S. Wortelboer, D. Frumin & J.A. Pérez

13

N 0,0 = case z (exp0 ⇒ c ← t 0,0 []; z ← t 1,0 [] c exp1 ⇒ c ← t 0,0 []; z ← t 0,1 [] c dup ⇒ c ← t 0,0 []; send z c; z ← t 0,0 [] ter ⇒ close z) N

1,0

= case z (ins0 ⇒ r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← p0,0 i [] r0 r1 a y)i∈LM exp0 ⇒ a.exp0 ; z ← t s,0 [0[]] a exp1 ⇒ a.dup; b ← recv a; a.exp1 ; b.exp0 ; z ← t 1,1 [] a b dup ⇒ a.dup; a′ ← recv a; c ← t 1,0 [] a; send z c; z ← t 1,0 [] a′ ter ⇒ a.1; wait a; close z)

N s,s = case z (ins0 ⇒ b.ter; wait b; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [α, β ] r0 r1 a y)i∈LM ins1 ⇒ a.ter; wait a; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [α, β ] r0 r1 b y)i∈LM exp0 ⇒ a.exp0 ; b.exp0 ; z ← t s,s [S[α], β ] a b exp1 ⇒ a.exp1 ; b.exp1 ; z ← t s,s [α, S[β ]] a b ter ⇒ a.ter; b.ter; wait a; wait b; close z) Figure 7: Examples of leaf, linear and binary nodes of the instantiation process (Definition 12).

for a counter and consequently is linear, a possible parent can represent a zero state for the same counter and be linear. Hence, duplication is needed so the parent can introduce new branches. • Node N s,s is a binary node that captures the state of incrementing state for both counters and the transition to a successor state for both. All states are variable expressions, and therefore, it uses open types; the process still needs to be instantiated with concrete values. For instantiation, it makes use of termination to remove the unused branch, as residual processes need to be terminated in ASP. Furthermore, because this is already a binary node, no new branches have to be created by either themselves or their parents; hence no implementation of duplication. To manage the tree, process definitions are added to the global environment ΣM . Note that Definition 12 depends on the process definitions given in Definition 11. Figure 8 illustrates how the decrement tree branches. The root node starts by duplicating its branch and then updating each branch using expansion to represent the different ways of decrementing. In turn, the branch with non-zero states will do the same, while the branch with a zero state will remain linear and forward the expansion. The expansions are terminated in the leaf node that becomes linear and creates a new leaf node. We are finally ready to encode the state of a machine, building upon the previous definitions. Definition 13 (Encoding state). Using Definitions 10 to 12, the encoding of state for machine M is

14

On the Expressiveness of Asynchronous Processes with Nested Session Types {|2, 1|}tM ′ {|2, 0|}tM {|2, 0|}M b0

{|1, 1|}M a0 exp1

{|1, 0|}M a0

M {|0, 1|}M a0 {|1, 0|}b 1

{|1, 0|}M a1

{|0, 0|}M {|0, 0|}M a2 a0

{|0, 0|}M a1

1

{|0, 0|}M a1

2

2

1

2

Figure 8: Example of branching of a linear node in Definition 12. Counter Process 0

Instruction Process incr

Jm0 Kr0

Instantiation Process

Ji | m0 , m1 KM r0 ,r1 ,t exp0

Jm0 + 1Kr′

{|m0 , m1 |}tM

0

Ji + 1 | m0 + 1, m1 KM r′ ,r1 ,t ′ 0

{|m0 + 1, m1 |}tM ′

Figure 9: An increment on counter 0. defined as: J(i, m0 , m1 )KM = Jm0 Kr0 , Jm1 Kr1 , {|m0 , m1 |}tM , Ji | m0 , m1 KM r0 ,r1 ,t

(5)

We use sequence diagrams to explain the encoding of the three possible steps of a machine. 1. Figure 9 shows how an incrementing reduction is mimicked. In the encoding, each process is able to predict the next state. Consequently, the instruction process simply sends the instruction to the counter (as denoted by the arrow with label incr) and then synchronises that change to the instantiation process (as denoted by the arrow with label exp0 ). Then, each process can move such that it matches the next state of the encoding. However, due to the concurrent, asynchronous nature of ASP, some processes (in particular the instruction process) can move ahead. Due to the properties of ASP, like type preservation, lagging processes are able to catch up without side effects, which only means that the encoding simply skipped a step but is still consistent. 2. Figure 10a shows the representation of a decrement. Unlike incrementing, the instruction process is not able to predict the next concrete state; it relies on the instantiation process to move to the next instruction. This is highlighted by the sending of the dependencies, followed by the forward, where the root node takes the place of the current instruction. Furthermore, a branch is promoted to become the new root node. Unlike incrementing, the instruction process has to wait for the instantiation process to catch up before it can proceed to instantiate the next instruction. 3. Finally, Figure 10b shows how we mimic jumping. Similar to the incrementing instruction, each

S. Wortelboer, D. Frumin & J.A. Pérez Counter Process 0

15 Instruction Process

decr

Jm0 Kr0

Instantiation Process

Ji | m0 , m1 KM r0 ,r1 ,t ins0

Jm0 − 1Kr′

{|m0 , m1 |}tM r0

0

r1 y (i + 1)

Ji + 1 | m0 − 1, m1 KM r′ ,r1 ,t ′

forward

0

{|m0 − 1, m1 |}tM ′

(a) A decrement: Counter 0 has value m0 > 0. Counter Process 0

Instruction Process

Instantiation Process

J0Kr0

Ji | 0, m1 KM r0 ,r1 ,t

{|0, m1 |}tM

J0Kr′

Jk | 0, m1 KM r′ ,r1 ,t

jump

0

0

(b) A jump: Counter 0 has value m0 = 0.

Figure 10: Encoding of a decrement-and-jump i : DECJ(0, k) on counter 0, as sequence diagrams. process can predict the next state; in this case, however, the state does not change. Instead, the instruction is simply sent, and afterwards we move to the next instruction k.

3.3

Correctness

Before illustrating our encoding (which we do in Section 3.4), we address its correctness. We first prove that the encoding is well-typed in ASP; hence, it inherits type preservation, progress, and confluence. Theorem 4 (Typability). Given any state (i, m0 , m1 )M we have: • · |=ΣM Jmi Kr :: (r : Lmi M)

(for i ∈ {0, 1}; cf. Definitions 7 and 10);

• · |=ΣM {|m0 , m1 |}tM :: (t : T M Lm0 , m1 M)

(cf. Definitions 9 and 12);

• r0 : Lm0 M, r1 : Lm1 M,t : T M Lm0 , m1 M, y : 1 |=ΣM Ji | m0 , m1 KM r0 ,r1 ,t :: (x : 1)

(cf Definition 11).

Hence, by Definition 13:

y : 1 |=ΣM J(i, m0 , m1 )KM :: (x : 1). Well-typedness of the encoding ensures not only that the properties of ASP hold, but also that the encoding follows the protocols for the individual components, as correctness is partially captured on the

16

On the Expressiveness of Asynchronous Processes with Nested Session Types

level of types. Theorem 4 is proved by induction on the value of the counter and case analysis on the instruction; see [23] for the full typing derivations. After establishing typability, the second step is to prove correspondence on the level of reductions. To prove such operational correspondence, we show that the semantics machine is simulated correctly (soundness) and that the encoding does not introduce any side effects (completeness). Theorem 5 (Soundness). Let (i, m0 , m1 ) be a state for a machine M. If (i, m0 , m1 ) −→M (i′ , m′0 , m′1 ), then J(i, m0 , m1 )KM −→+ J(i′ , m′0 , m′1 )KM .

The proof of Theorem 5 follows largely from the construction of the stateful session types, which capture the semantics with regard to transitions of state for different instructions. As the encoding is well-typed (Theorem 4) as long as the correct instruction is sent in correspondence with the current state i, the encoding behaves the same as the machine concerning soundness. This leaves the validation of the correct instruction being executed. This is relatively easy to verify, as in the encoding, each instruction is prefixed with the sending of a correct label over the correct channel, with no further interaction between the instruction and counter process until the next instruction. The correctness of the next instruction follows in cases of incrementing and jumping, as the next instruction is immediately instantiated. The case of decrementing is different, as it makes use of the instantiation process; however, as such an instruction sends the label for the next instruction and the instantiation process takes this label to instantiate the correct next instruction, it is clear that, from this perspective, the encoding behaves correctly. Because the encoding is well-typed, progress is guaranteed except over channel y, which is there to simulate termination for out-of-bound instructions. The proof of soundness is further illustrated by the sequence diagrams in Figures 9 and 10. Note: the diagrams focus on the sequence of the reductions that lead to the next state of an encoding such that it matches the one-step source reduction in the machine. Theorem 6 (Completeness). Suppose J(i, m0 , m1 )KM −→+ S where S is a configuration in ASP. Then ′ ′ ′ there exists (i′ , m′0 , m′1 ) such that S −→+ J(i′ , m′0 , m′1 )KM and (i, m0 , m1 ) −→+ M (i , m0 , m1 ). The proof of Theorem 6 follows the same structure as the proof of soundness (Theorem 5), using the fact that ASP is confluent. Essentially, if a translation of the machine state reduces to some configuration S, then S can further reduce to a translation of another machine state. This follows from reordering of the reductions as a consequence of confluence and soundness. As mentioned in the discussion of the sequence diagrams, it is entirely possible for a process like that of the instruction to move ahead without waiting for the counter to match the encoding first. In the context of ASP each of these reductions can always be applied at a later state to match the encoding; at no point can other processes influence the reduction to the next state for such a process. Hence, again, this is simply a reordering of the order of reductions that was found in the proof of soundness.

3.4

Examples

To illustrate the behaviour of the encoding and our operational correspondence results, we consider the translation of a simple machine M: {(1 : INC(1)), (2 : INC(0)), (3 : DECJ(1, 2))}. Depending on the starting instruction, M can exhibit both terminating and non-terminating behaviour: • Terminating computation: (1, 0, 0) −→M (2, 0, 1) −→M (3, 1, 1) −→M (4, 1, 0) ̸−→M

S. Wortelboer, D. Frumin & J.A. Pérez

17

• Non-terminating computation: (2, 0, 0) −→M (3, 1, 0) −→M (2, 1, 0) −→M · · · The first computation terminates because of the initial increment, which allows the decrement instruction to succeed and move out-of-bounds. In the second computation this initial increment is skipped; as a result, the decrement fails and jumps back to the initial instruction, allowing it to loop continuously. The sequence diagrams in Figures 9 and 10 help visualise how, for each step in the machine, a set of reductions in the encoding can be composed such that it leads to the encoded next state, justifying soundness for the encoding of the two computations. There is a difference: the terminating computation makes use of the instantiation process to move to the next instruction, while the non-terminating computation does not use it, as the decrement fails and the state does not change. Because of the asynchronous nature of ASP, the instruction process in the encoding can move independently from the other processes until it requires something of them in case of decrements. This can be illustrated by the encoding of the terminating computation, which follows the flow of Figure 9: J(1, 0, 0)KM −→+ J0Kr0 , msg(r0′ , r0 .incr; r0′ ↔ r0 ),

J0Kr1 , msg(r1′ , r1 .incr; r1′ ↔ r1 ),

{|0, 0|}tM , msg(t 1 ,t.exp1 ; t 1 ↔ t), msg(t 2 ,t 1 .exp0 ; t 2 ↔ t 1 ), J3 | 1, 1KM r0′ ,r1′ ,t 2 | {z } St

where −→+ denotes to the transitive closure of −→. Here, the encoding of the instruction is already at the state (3, 1, 1). At this point, the consumption of all messages would allow the encoding to match for all other processes. However, there is nothing preventing the process from not doing so, except when the instruction reduces further, following Figure 10a: + ′′ ′ ′′ ′ 3 2 3 2 ′ ′ J3 | 1, 1KM r0′ ,r1′ ,t 2 −→ msg(r0 , r0 .decr; r0 ↔ r0 ), msg(t ,t .ins1 ; t ↔ t ), · · · , msg(x,t .4; x ↔ t ) {z } | Si

Because the protocol allows for a successful decrement, the current instruction hands over to the instruction process, as that process is aware of the state after decrementing the counter; this is done by sending the dependencies, the label for the next instruction and the channel that the instruction process offers. The only reductions possible are those of the consumption of messages, in particular those of the instantiation process, as they construct the next instruction. This continues the flow of Figure 10a. 3 2 3 2 ′ ′ St , Si −→+ {|1, 1|}tM 2 , msg(t ,t .ins1 ; t ↔ t ), · · · , msg(x,t .4; x ↔ t )

= {|0, 1|}tM , {|1, 0|}tM , proc(t 2 , N 1,1 ), msg(t 3 ,t 2 .ins1 ; t 3 ↔ t 2 ), · · · , msg(x,t ′ .4; x ↔ t ′ ) 0 1 −→+ {|1, 0|}tM , J4 | 1, 0KM r′′ ,r′ ,t1 1 0

1

When we skip ahead to the instantiation steps (for branching, see Figure 8), then what is left is for the process associated to branch 0, 1 to terminate and instantiate the next instruction, using the branch 1, 0 and the dependencies received from previous instruction. In this case, instruction 4 is out-of-bounds: the instruction process becomes poised over channel y; when the reductions of the counters take place (Figures 9 and 10a), the encoding matches the machine state (4, 1, 0). In the encoding of the non-terminating computation, this final synchronisation never happens; moreover, it never decrements, and so the instruction never makes use of the instantiation process. This means that increment and jump messages to the counter and the expand messages to the instantiation process just queue up. But at any point, they can be consumed such that the encoding can match the state of the simulated machine.

18

On the Expressiveness of Asynchronous Processes with Nested Session Types

Notable in this example is that instructions never require anything from the counter and merely update their state. While at the process level the counters serve little function, their use comes from the session types they implement, enforcing the correct behaviour of processes using them. They essentially represent the possible reductions with state transitions independent of the definition of the instructions.

4

Concluding Remarks

We have studied the expressiveness of ASP, the asynchronous process language associated with the Nested Session Types by Das et al.. Starting from an intuitive encoding of numbers that naturally leverages nested types that implement Peano’s representation of the naturals (Definition 7), we encoded Minsky machines by developing instruction processes that are state-aware in order to precisely and correctly enact decrement-and-jump instructions. The correctness properties of our encoding are given in terms of typability (Theorem 4) and operational correspondence (soundness and completeness guarantees, cf. Theorems 5 and 6). Combined, these results entail that the coupling of ASP and NSTs is Turing complete. In future work, we would like to explore connections between ASP (and NSTs) with other typed languages with logical foundations, such as CLASS [20, 7], which features both polymorphism and state.

Related Work Closely related work has been discussed in the introduction; here we comment on other relevant literature. Minsky machines are a convenient model for proving the Turing completeness of models of concurrency. They were used, for instance, by Busi et al. [4, 5, 6] to compare different forms of infinite behaviour in CCS and by Lanese et al. [17, 18] to establish the expressiveness of higher-order process calculi. In both cases, the calculi are untyped. In typed process calculi, the situation is different, as types enforce correctness by considerably narrowing down the kind of (non-terminating) behaviours that well-typed processes can express. We are not aware of other typed encodings of Minsky machines. In linearly-typed calculi, the limited flexibility is even more prominent, as linearity induces properties such as confluence and deadlock freedom. This is the case for typed frameworks derived from the CurryHoward correspondence between session types and linear logic [8], which are strongly normalising. In this respect, the work of Balzer et al. [3] is related: they consider a session-typed π-calculus with manifest sharing, and show that adding recursive shared types to an otherwise linearly-typed language suffices to correctly encode the untyped, asynchronous π-calculus. Also in the typed setting, Kouzapas et al. [15, 16] obtain a series of relative expressiveness results concerning first- and higher-order π-calculi with session types (not based on linear logic). They discover that non-tail recursive types are essential to encode a name-passing calculus into a higher-order calculus. From this perspective, advanced type disciplines such as NSTs bring substantial expressive power, beyond usual recursive types [11]; still, it is interesting to note that correctly encoding Minsky machines is not trivial, even when counting with the power of (nested) recursion and polymorphism in types.

Acknowledgments We are grateful to the anonymous reviewers for their constructive feedback. This research has been partially supported by the Dutch Research Council (NWO) under project “Cyclic Structures in Programs and Proofs” (OCENW.XL.23.089).

S. Wortelboer, D. Frumin & J.A. Pérez

19

References [1] Bernardo Almeida, Andreia Mordido, Peter Thiemann & Vasco T. Vasconcelos (2022): Polymorphic lambda calculus with context-free session types. Inf. Comput. 289(Part), p. 104948, doi:10.1016/J.IC.2022.104948. Available at https://doi.org/10.1016/j.ic.2022.104948. [2] Bernardo Almeida, Andreia Mordido & Vasco T. Vasconcelos (2020): Deciding the Bisimilarity of ContextFree Session Types. In Armin Biere & David Parker, editors: Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, Lecture Notes in Computer Science 12079, Springer, pp. 39–56, doi:10.1007/978-3-030-45237-7_3. Available at https://doi.org/10.1007/978-3-030-45237-7_3. [3] Stephanie Balzer, Frank Pfenning & Bernardo Toninho (2018): A Universal Session Type for Untyped Asynchronous Communication. In Sven Schewe & Lijun Zhang, editors: 29th International Conference on Concurrency Theory, CONCUR 2018, Beijing, China, September 4-7, 2018, LIPIcs 118, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 30:1–30:18, doi:10.4230/LIPICS.CONCUR.2018.30. Available at https://doi.org/10.4230/LIPIcs.CONCUR.2018.30. [4] Nadia Busi, Maurizio Gabbrielli & Gianluigi Zavattaro (2003): Replication vs. Recursive Definitions in Channel Based Calculi. In Jos C. M. Baeten, Jan Karel Lenstra, Joachim Parrow & Gerhard J. Woeginger, editors: Automata, Languages and Programming, 30th International Colloquium, ICALP 2003, Eindhoven, The Netherlands, June 30 - July 4, 2003. Proceedings, Lecture Notes in Computer Science 2719, Springer, pp. 133–144, doi:10.1007/3-540-45061-0_12. Available at https://doi.org/10.1007/3-540-45061-0_12. [5] Nadia Busi, Maurizio Gabbrielli & Gianluigi Zavattaro (2004): Comparing Recursion, Replication, and Iteration in Process Calculi. In Josep Díaz, Juhani Karhumäki, Arto Lepistö & Donald Sannella, editors: Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July 1216, 2004. Proceedings, Lecture Notes in Computer Science 3142, Springer, pp. 307–319, doi:10.1007/9783-540-27836-8_28. Available at https://doi.org/10.1007/978-3-540-27836-8_28. [6] Nadia Busi, Maurizio Gabbrielli & Gianluigi Zavattaro (2009): On the expressive power of recursion, replication and iteration in process calculi. Math. Struct. Comput. Sci. 19(6), pp. 1191–1222, doi:10.1017/S096012950999017X. Available at https://doi.org/10.1017/S096012950999017X. [7] Luís Caires (2025): Thread and Memory-Safe Programming with CLASS. In Farzaneh Derakhshan & Jan Hoffmann, editors: Proceedings 16th International Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software, PLACES@ETAPS 2025, Hamilton, Canada, 4th May 2025, EPTCS 420, pp. 22–33, doi:10.4204/EPTCS.420.3. Available at https://doi.org/10.4204/ EPTCS.420.3. [8] Luís Caires & Frank Pfenning (2010): Session Types as Intuitionistic Linear Propositions. In Paul Gastin & François Laroussinie, editors: CONCUR 2010 - Concurrency Theory, 21th International Conference, CONCUR 2010, Paris, France, August 31-September 3, 2010. Proceedings, Lecture Notes in Computer Science 6269, Springer, pp. 222–236, doi:10.1007/978-3-642-15375-4_16. Available at https://doi.org/10. 1007/978-3-642-15375-4_16. [9] Ankush Das, Henry DeYoung, Andreia Mordido & Frank Pfenning (2021): Nested Session Types. In Nobuko Yoshida, editor: Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Lecture Notes in Computer Science 12648, Springer, pp. 178–206, doi:10.1007/978-3-030-72019-3_7. Available at https://doi.org/10. 1007/978-3-030-72019-3_7. [10] Ankush Das, Henry DeYoung, Andreia Mordido & Frank Pfenning (2022): Nested Session Types. ACM Trans. Program. Lang. Syst. 44(3), pp. 19:1–19:45, doi:10.1145/3539656. Available at https://doi.org/ 10.1145/3539656.

20

On the Expressiveness of Asynchronous Processes with Nested Session Types

[11] Simon J. Gay, Diogo Poças & Vasco T. Vasconcelos (2022): The Different Shades of Infinite Session Types. In Patricia Bouyer & Lutz Schröder, editors: Foundations of Software Science and Computation Structures 25th International Conference, FOSSACS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Lecture Notes in Computer Science 13242, Springer, pp. 347–367, doi:10.1007/978-3-030-99253-8_18. Available at https: //doi.org/10.1007/978-3-030-99253-8_18. [12] Kohei Honda (1993): Types for Dyadic Interaction. In Eike Best, editor: CONCUR ’93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, Lecture Notes in Computer Science 715, Springer, pp. 509–523, doi:10.1007/3-540-57208-2_35. Available at https: //doi.org/10.1007/3-540-57208-2_35. [13] Kohei Honda, Vasco Thudichum Vasconcelos & Makoto Kubo (1998): Language Primitives and Type Discipline for Structured Communication-Based Programming. In Chris Hankin, editor: Programming Languages and Systems - ESOP’98, 7th European Symposium on Programming, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, Lecture Notes in Computer Science 1381, Springer, pp. 122–138, doi:10.1007/BFB0053567. Available at https://doi.org/10.1007/BFb0053567. [14] C. Jennings, R. Mahy & A. B. Roach (2007): Relay Extensions for the Message Sessions Relay Protocol (MSRP). RFC 4976, doi:10.17487/RFC4976. Available at https://www.rfc-editor.org/info/ rfc4976/. [15] Dimitrios Kouzapas, Jorge A. Pérez & Nobuko Yoshida (2016): On the Relative Expressiveness of HigherOrder Session Processes. In Peter Thiemann, editor: Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Lecture Notes in Computer Science 9632, Springer, pp. 446–475, doi:10.1007/978-3-662-49498-1_18. Available at https://doi.org/10.1007/978-3-662-49498-1_18. [16] Dimitrios Kouzapas, Jorge A. Pérez & Nobuko Yoshida (2019): On the relative expressiveness of higherorder session processes. Inf. Comput. 268, doi:10.1016/J.IC.2019.06.002. Available at https://doi.org/ 10.1016/j.ic.2019.06.002. [17] Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi & Alan Schmitt (2008): On the Expressiveness and Decidability of Higher-Order Process Calculi. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, IEEE Computer Society, pp. 145–155, doi:10.1109/LICS.2008.8. Available at https://doi.org/10.1109/LICS.2008.8. [18] Ivan Lanese, Jorge A. Pérez, Davide Sangiorgi & Alan Schmitt (2011): On the expressiveness and decidability of higher-order process calculi. Inf. Comput. 209(2), pp. 198–226, doi:10.1016/J.IC.2010.10.001. Available at https://doi.org/10.1016/j.ic.2010.10.001. [19] Marvin L. Minsky (1967): Computation: finite and infinite machines. Prentice-Hall, Inc., USA. [20] Pedro Rocha & Luís Caires (2023): Safe Session-Based Concurrency with Shared Linear State. In Thomas Wies, editor: Programming Languages and Systems - 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Lecture Notes in Computer Science 13990, Springer, pp. 421–450, doi:10.1007/978-3-031-30044-8_16. Available at https://doi.org/10.1007/ 978-3-031-30044-8_16. [21] Gil Silva, Andreia Mordido & Vasco T. Vasconcelos (2023): Subtyping Context-Free Session Types. In Guillermo A. Pérez & Jean-François Raskin, editors: 34th International Conference on Concurrency Theory, CONCUR 2023, Antwerp, Belgium, September 18-23, 2023, LIPIcs 279, Schloss Dagstuhl - LeibnizZentrum für Informatik, pp. 11:1–11:19, doi:10.4230/LIPICS.CONCUR.2023.11. Available at https: //doi.org/10.4230/LIPIcs.CONCUR.2023.11. [22] Peter Thiemann & Vasco T. Vasconcelos (2016): Context-free session types. In Jacques Garrigue, Gabriele Keller & Eijiro Sumii, editors: Proceedings of the 21st ACM SIGPLAN International Confer-

S. Wortelboer, D. Frumin & J.A. Pérez

21

ence on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, ACM, pp. 462–475, doi:10.1145/2951913.2951926. Available at https://doi.org/10.1145/2951913.2951926. [23] Sjors Wortelboer (2026): Nested Session Types in Turing Complete Calculi. Master’s thesis, University of Groningen. Available at https://jperez.nl/files/MScThesis-Wortelboer.pdf. Accessed: 202606-28.

22

On the Expressiveness of Asynchronous Processes with Nested Session Types

A

Additional Material for Section 2

A.1

Type rules ASP (Definition 3)

Type rules for processes P: (k ∈ L) V; ∆ ⊢ P :: (x : Ak ) ⊕R V; ∆ ⊢ x.k; P :: (x : ⊕{l ⇒ Al }l∈L )

(∀l ∈ L) V; ∆, x : Al ⊢ Ql :: (z : C) ⊕L V; ∆, x : ⊕{l : Al }l∈L ⊢ case x (l ⇒ Ql )l∈L :: (z : C)

(∀l ∈ L) V; ∆ ⊢ Pl :: (x : Al ) &R V; ∆ ⊢ case x (l ⇒ Ql )l∈L :: (x : &{l ⇒ Al }l∈L ) (k ∈ L) V; ∆ ⊢ P :: (x : Ak ) &L V; ∆, x : &{l ⇒ Al }l∈L ⊢ x.k; Q :: (z : C)

·; V ⊢ A ≡ A′ V; ∆ ⊢ P :: (x : B) ⊗R V; ∆, y : A ⊢ send x y; P :: (x : A′ ⊗ B)

V; ∆, y : A, x : B ⊢ Q :: (z : C) ⊗L V; ∆, x : A ⊗ B ⊢ y ← recv x; Q :: (z : C)

V; ∆, y : A ⊢ P :: (x : B) ⊸R V; ∆ ⊢ y ← recv x; P :: (x : A ⊸ B)

·; V ⊢ A ≡ A′ V; ∆, x : B ⊢ Q :: (z : C) ⊸L ′ V; ∆, x : A ⊸ B, y : A ⊢ send x y; Q :: (z : C)

·; · ⊢ close x :: (x : 1)

1R

·; V ⊢ A ≡ A′ id V; y : A ⊢ x ↔ y :: (x : A′ )

V; ∆ ⊢ Q :: (z : C) 1L V; ∆, x : 1 ⊢ wait x; Q :: (z : C)

y′ : B′ ⊢ f [α] = Pf :: (x′ : B) ∈ Σ ·; V ⊢ ∆′ ≡ y : B′ [θ ] V; ∆, x : B[θ ] ⊢ Q :: (z : C) def ′ V; ∆, ∆ ⊢ x ← f [θ ] y; Q :: (z : C) Type rules for messages M: ·; x′ : A

(k ∈ L) &M ·; x : &{l : Al }l∈L ⊢ x.k; x′ ↔ x :: (x′ : Ak )

(k ∈ L) ⊕M ′ k ⊢ x.k; x ↔ x :: (x : ⊕{l : Al }l∈L ) ·; · ⊢ A ≡ A′

·; y : A, x′ : B ⊢ send x y; x ↔ x′ :: (x : A′ ⊗ B) ·; · ⊢ A ≡ A′ ⊸M ·; x : A′ ⊸ B, y : A ⊢ send x y; x′ ↔ x :: (x′ : B)

A.2

⊗M

·; · ⊢ close x :: (x : 1)

1M

Reduction rules for ASP (Definition 5) proc(x, x.k; P) −→ proc(x′ , P[x′ /x]), msg(x, x.k; x ↔ x′ )

(⊕S)

′

′

msg(x, x.k; x ↔ x ), proc(y, case x (l ⇒ Ql )) −→ proc(y, Qk [x /x])

(⊕C)

proc(d, x.k; P) −→ msg(x, x.k; x ↔ x′ ), proc(d, P[x′ /x])

(&S)

′

′

′

proc(x, case x (l ⇒ Ql )), msg(x, x.k; x ↔ x ) −→ proc(x , Qk [x /x])

(&C)

S. Wortelboer, D. Frumin & J.A. Pérez

23

proc(x, send x w; P) −→ proc(x′ , P[x′ /x]), msg(x, send x w; x ↔ x′ ) ′

′

′

(⊗S) ′

msg(x, send x w; x ↔ x ), proc(y, w ← recv x; Q) −→ proc(y, Q[x /x, w/w ])

(⊗C)

proc(y, send x w; P) −→ msg(x, send x w; x ↔ x′ ), proc(y, P[x′ /x])

(⊸ S)

′

′

′

′

′

proc(x, w ← recv x; Q), msg(x, send x w; x ↔ x ) −→ proc(x , Q[x /x, w/w ])

(⊸ C)

proc(x, close x) −→ msg(x, close x)

(1S)

msg(x, close x), proc(y, wait x; P) −→ proc(y, P)

(1C)

msg(d, M), proc(c, c ↔ d) −→ msg(c, M[c/d])

(id+ C)

proc(c, c ↔ d), msg(e, Mc ) −→ msg(e, Mc [d/c])

(id− C)

proc(d, Q), proc(c, c ↔ d) −→ proc(c, Q[c/d])

(id+ S)

proc(c, c ↔ d), proc(e, Qc ) −→ proc(e, Qc [d/c])

(id− S)

proc(z, x ← f [θ ] d; Q) −→ proc(a, Pf [a/x, d/y, θ ]), proc(z, Q[a/x])

(defC)

B

Additional Material for Section 3

B.1

Constituent process definitions (Definition 12) N 0,0 = case z (exp0 ⇒ c ← t 0,0 []; z ← t 1,0 [] c exp1 ⇒ c ← t 0,0 []; z ← t 0,1 [] c dup ⇒ c ← t 0,0 []; send z c; z ← t 0,0 [] ter ⇒ close z) N 1,0 = case z (ins0 ⇒ r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← p0,0 i [] r0 r1 a y)i∈LM exp0 ⇒ a.exp0 ; z ← t s,0 [0[]] a exp1 ⇒ a.dup; b ← recv a; a.exp1 ; b.exp0 ; z ← t 1,1 [] a b dup ⇒ a.dup; a′ ← recv a; c ← t 1,0 [] a; send z c; z ← t 1,0 [] a′ ter ⇒ a.1; wait a; close z) N

s,0

= case z (ins0 ⇒ r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,0 i [α] r0 r1 a y)i∈LM exp0 ⇒ a.exp0 ; z ← t s,0 [S[α]] a exp1 ⇒ a.dup; b ← recv a; a.exp1 ; b.exp0 ; z ← t s,1 [α] a b dup ⇒ a.dup; b ← recv a; c ← t s,0 [α] a; send z c; z ← t s,0 [α] b ter ⇒ a.ter; wait a; close z)

24

On the Expressiveness of Asynchronous Processes with Nested Session Types N 0,1 = case z (ins1 ⇒ r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← p0,0 i [] r0 r1 b y)i∈LM exp0 ⇒ b.dup; a ← recv b; a.exp1 ; b.exp0 ; z ← t 1,1 [] a b exp1 ⇒ b.exp1 ; z ← t 0,s [0[]] b dup ⇒ a.dup; a′ ← recv a; c ← t 0,1 [] a; send z c; z ← t 0,1 [] a′ ter ⇒ b.1; wait b; close z) N

0,s

= case z (ins1 ⇒ r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,0 i [α] r0 r1 a y)i∈LM exp0 ⇒ b.dup; a ← recv b; b.exp1 ; a.exp0 ; z ← t 1,s [β ] b a exp1 ⇒ b.exp1 ; z ← t 0,s [S[β ]] a dup ⇒ b.dup; a ← recv b; c ← t 0,s [β ] b; send z c; z ← t 0,s [β ] a ter ⇒ b.ter; wait b; close z)

N

1,1

= case z (ins0 ⇒ b.ter; wait b; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← p0,s i [α] r0 r1 a y)i∈LM ins1 ⇒ a.ter; wait a; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,0 i [α] r0 r1 b y)i∈LM exp0 ⇒ a.exp0 ; b.exp0 ; z ← t s,1 [0[]] a b exp1 ⇒ a.exp1 ; b.exp1 ; z ← t 1,s [0[]] a b ter ⇒ a.ter; b.ter; wait a; wait b; close z)

N

s,1

= case z (ins0 ⇒ b.ter; wait b; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [α] r0 r1 a y)i∈LM ins1 ⇒ a.ter; wait a; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,0 i [α] r0 r1 b y)i∈LM exp0 ⇒ a.exp0 ; b.exp0 ; z ← t s,1 [S[α]] a b exp1 ⇒ a.exp1 ; b.exp1 ; z ← t s,s [α, 0[]] a b ter ⇒ a.ter; b.ter; wait a; wait b; close z)

N

1,s

= case z (ins0 ⇒ b.ter; wait b; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← p0,s i [β ] r0 r1 a y)i∈LM ins1 ⇒ a.ter; wait a; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [β ] r0 r1 b y)i∈LM exp0 ⇒ a.exp0 ; b.exp0 ; z ← t s,s [0[], β ] a b exp1 ⇒ a.exp1 ; b.exp1 ; z ← t 1,s [S[β ]] a b ter ⇒ a.ter; b.ter; wait a; wait b; close z)

S. Wortelboer, D. Frumin & J.A. Pérez N s,s = case z (ins0 ⇒ b.ter; wait b; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [α, β ] r0 r1 a y)i∈LM ins1 ⇒ a.ter; wait a; r0 ← recv z; r1 ← recv z; y ← recv z; case z (i ⇒ z ← ps,s i [α, β ] r0 r1 b y)i∈LM exp0 ⇒ a.exp0 ; b.exp0 ; z ← t s,s [S[α], β ] a b exp1 ⇒ a.exp1 ; b.exp1 ; z ← t s,s [α, S[β ]] a b ter ⇒ a.ter; b.ter; wait a; wait b; close z)

25

Related documents

• On the Expressiveness of Asynchronous Processes with Nested Session Types#1447925
• NEST: Network Enforced Session Types#367511
• Session Initiation Protocol (SIP) Extension for Event State Publication#133574
• Requirements for Resource Priority Mechanisms for the Session Initiation Protocol (SIP)#193111
• SIP: Session Initiation Protocol#132747