Domain-Aware Session Types (Extended Version)
Lu\'is Caires, Jorge A. P\'erez, Frank Pfenning, Bernardo Toninho
TL;DR
This paper introduces a novel framework for domain-aware session types using an extension of linear logic with modal worlds, enabling expressive, safe, and flexible message-passing concurrency with domain migration.
Contribution
It generalizes existing session types by incorporating domain-awareness through modal logic, allowing dynamic domain information and nested protocols with formal correctness guarantees.
Findings
Ensures session fidelity, progress, and termination for well-typed processes.
Supports runtime domain information and flexible accessibility relations.
Provides a reduction-based analysis for complex multiparty protocols.
Abstract
We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation. Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Security and Verification in Computing
\hideLIPIcs
Universidade Nova de Lisboa 0000-0002-3215-6734
University of Groningen https://orcid.org/0000-0002-1452-6180
Carnegie Mellon University
Universidade Nova de Lisboa https://orcid.org/0000-0002-0746-7514 \fundingCaires and Toninho are supported by NOVA LINCS (Ref. UID/CEC/04516/2019). Pérez is supported by the NWO VIDI Project No. 016.Vidi.189.046. Pfenning is supported by NSF Grant No. CCF-1718267: “Enriching Session Types for Practical Concurrent Programming”.
\ccsdesc[500]Theory of computation Process calculi \ccsdesc[100]Theory of computation Type structures \ccsdesc[100]Software and its engineering Message passing \CopyrightCaires et al.
\EventEditorsWan Fokkink and Rob van Glabbeek \EventNoEds2 \EventLongTitle30th International Conference on Concurrency Theory (CONCUR 2019) \EventShortTitleCONCUR 2019 \EventAcronymCONCUR \EventYear2019 \EventDateAugust 27–30, 2019 \EventLocationAmsterdam, the Netherlands \EventLogo \SeriesVolume140 \ArticleNo35
Domain-Aware Session Types (Extended Version)
Luís Caires
Jorge A. Pérez
Frank Pfenning
Bernardo Toninho
Abstract
We develop a generalization of existing Curry-Howard interpretations of (binary) session types by relying on an extension of linear logic with features from hybrid logic, in particular modal worlds that indicate domains. These worlds govern domain migration, subject to a parametric accessibility relation familiar from the Kripke semantics of modal logic. The result is an expressive new typed process framework for domain-aware, message-passing concurrency. Its logical foundations ensure that well-typed processes enjoy session fidelity, global progress, and termination. Typing also ensures that processes only communicate with accessible domains and so respect the accessibility relation.
Remarkably, our domain-aware framework can specify scenarios in which domain information is available only at runtime; flexible accessibility relations can be cleanly defined and statically enforced. As a specific application, we introduce domain-aware multiparty session types, in which global protocols can express arbitrarily nested sub-protocols via domain migration. We develop a precise analysis of these multiparty protocols by reduction to our binary domain-aware framework: complex domain-aware protocols can be reasoned about at the right level of abstraction, ensuring also the principled transfer of key correctness properties from the binary to the multiparty setting.
keywords:
Session Types, Linear Logic, Process Calculi, Hybrid Logic
1 Introduction
The goal of this paper is to show how existing Curry-Howard interpretations of session types [9, 10] can be generalized to a domain-aware setting by relying on an extension of linear logic with features from hybrid logic [42, 5]. These extended logical foundations of message-passing concurrency allow us to analyze complex domain-aware concurrent systems (including those governed by multiparty protocols) in a precise and principled manner.
Software systems typically rely on communication between heterogeneous services; at their heart, these systems rely on message-passing protocols that combine mobility, concurrency, and distribution. As distributed services are often virtualized, protocols should span diverse software and hardware domains. These domains can have multiple interpretations, such as the location where services reside, or the principals on whose behalf they act. Concurrent behavior is then increasingly domain-aware: a partner’s potential for interaction is influenced not only by the domains it is involved in at various protocol phases (its context), but also by connectedness relations among domains. Moreover, domain architectures are rarely fully specified: to aid modularity and platform independence, system participants (e.g., developers, platform vendors, service clients) often have only partial views of actual domain structures. Despite their importance in communication correctness and trustworthiness at large, the formal status of domains within typed models of message-passing systems remains unexplored.
This paper contributes to typed approaches to the analysis of domain-aware communications, with a focus on session-based concurrency. This approach specifies the intended message-passing protocols as session types [29, 30, 23]. Different type theories for binary and multiparty (-ary) protocols have been developed. In both cases, typed specifications can be conveniently coupled with -calculus processes [36], in which so-called session channels connect exactly two subsystems. Communication correctness usually results from two properties: session fidelity (type preservation) and deadlock freedom (progress). The former says that well-typed processes always evolve to well-typed processes (a safety property); the latter says that well-typed processes will never get into a stuck state (a liveness property).
A key motivation for this paper is the sharp contrast between (a) the growing relevance of domain-awareness in message-passing, concurrent systems and (b) the expressiveness of existing session type frameworks, binary and multiparty, which cannot adequately specify (let alone enforce) domain-related requirements. Indeed, existing session types frameworks, including those based on Curry-Howard interpretations [9, 50, 13], capture communication behavior at a level of abstraction in which even basic domain-aware assertions (e.g., “Shipper resides in domain AmazonUS”) cannot be expressed. As an unfortunate consequence, the effectiveness of the analysis techniques derived from these frameworks is rather limited.
To better illustrate our point, consider a common distributed design pattern: a middleware agent () which answers requests from clients (), sometimes offloading the requests to a server () to better manage local resource availability. In the framework of multiparty session types [31] this protocol can be represented as the global type:
[TABLE]
The client first sends a request to the middleware, which answers back with either a message containing the answer or a message, signaling that the server will be contacted to produce the final . While this multiparty protocol captures the intended communication behavior, it does not capture that protocols for the middleware and the server often involve some form of privilege escalation or specific authentication—ensuring, e.g., that the server interaction is adequately isolated from the client, or that the escalation must precede the server interactions. These requirements simply cannot be represented in existing frameworks.
Our work addresses this crucial limitation by generalizing Curry-Howard interpretations of session types by appealing to hybrid logic features. We develop a logically motivated typed process framework in which worlds from modal logics precisely and uniformly define the notion of domain in session-based concurrency. At the level of binary sessions, domains manifest themselves through point-to-point domain migration and communication. In multiparty sessions, domain migration is specified choreographically through the new construct , where participant leads a migration of participants to domain in order to perform protocol , who then migrate back to perform protocol .
Consider the global type in our previous example. Our framework allows us to refactor the global type above as:
[TABLE]
By considering a first-class multiparty domain migration primitive at the type and process levels, we can specify that the offload portion of the protocol takes place after the middleware and the server migrate to a private domain , as well as ensuring that only accessible domains can be interacted with. For instance, the type for the server that is mechanically projected from the protocol above ensures that the server first migrates to the private domain, communicates with the middleware, and then migrates back to its initial domain.
Perhaps surprisingly, our domain-aware multiparty sessions are studied within a context of logical binary domain-aware sessions, arising from a propositions-as-types interpretation of hybrid linear logic [21, 17], with strong static correctness guarantees derived from the logical nature of the system. Multiparty domain-awareness arises through an interpretation of multiparty protocols as medium processes [7] that orchestrate the multiparty interaction while enforcing the necessary domain-level constraints and migration steps.
Contributions
The key contributions of this work are:
A process model with explicit domain-based migration (§ 2). We present a session -calculus with domains that can be communicated via novel domain movement prefixes. 2. 2.
A session type discipline for domain-aware interacting processes (§ 3). Building upon an extension of linear logic with features from hybrid logic [21, 17] we generalize the Curry-Howard interpretation of session types [9, 10] by interpreting (modal) worlds as domains where session behavior resides. In our system, types can specify domain migration and communication; domain mobility is governed by a parametric accessibility relation. Judgments stipulate the services used and realized by processes and the domains where sessions should be present. Our type discipline statically enforces session fidelity, global progress and, notably, that communication can only happen between accessible domains. 3. 3.
As a specific application, we introduce a framework of domain-aware multiparty sessions (§ 4) that uniformly extends the standard multiparty session framework of [31] with domain-aware migration and communication primitives. Our development leverages our logically motivated domain-aware binary sessions (§ 3) to give a precise semantics to multiparty sessions through a (typed) medium process that acts as an orchestrator of domain-aware multiparty interactions, lifting the strong correctness properties of typed processes to the multiparty setting. We show that mediums soundly and completely encode the local behaviors of participants in a domain-aware multiparty session.
We conclude with a discussion of related work (§ 5) and concluding remarks (§ 6). Appendix A lists omitted definitions and proofs. We point the interested reader to Appendices B and C for extended examples on domain-aware multiparty and binary sessions, respectively.
2 Process Model
We introduce a synchronous -calculus [44] with labeled choice and explicit domain migration and communication. We write to stand for a concrete domain () or a domain variable (). Domains are handled at a high-level of abstraction, with their identities being attached to session channels. Just as the -calculus allows for communication over names and name mobility, our model also allows for domain communication and mobility. These features are justified with the typing discipline of § 3.
Definition 2.1**.**
Given infinite, disjoint sets of names , of labels , of domain tags and of domain variables , respectively, the set of processes is defined by
[TABLE]
Domain-aware prefixes are present only in the last line. As we make precise in the typed setting of § 3, these constructs realize mobility and domain communication, in the usual sense of the -calculus: migration to a domain is always associated to mobility with a fresh name.
The operators (inaction), (parallel composition) and (name restriction) are standard. We then have (send on and proceed as ), (receive on and proceed as with parameter replaced by ), and which denotes replicated (persistent) input. The forwarding construct equates and ; it is a primitive representation of a copycat process. The last two constructs in the second line define a labeled choice mechanism: x\triangleright\!\big{\{}\mathit{l}_{i}:P_{i}\big{\}}_{i\in I} is a process that awaits some label (with ) and proceeds as . Dually, the process emits a label and proceeds as .
The first two operators in the third line define explicit domain migration: given a domain , denotes a process that is prepared to migrate the communication actions in on endpoint , to session on . Complementarily, process signals an endpoint to move to , providing with the appropriate session endpoint that is then bound to . In a typed setting, domain movement will be always associated with a fresh session channel. Alternatively, this form of coordinated migration can be read as an explicit form of agreement (or authentication) in trusted domains. Finally, the last two operators in the third line define output and input of domains, and , respectively. These constructs allow for domain information to be obtained and propagated across processes dynamically.
Following [43], we abbreviate and as and , respectively. In , , and the distinguished occurrence of name is binding with scope . Similarly for in . We identify processes up to consistent renaming of bound names and variables, writing for this congruence. P\{\raisebox{2.15277pt}{\smallx}\!/\mbox{\smally}\} denotes the capture-avoiding substitution of for in . While structural congruence expresses standard identities on the basic structure of processes (cf. [longversion]), reduction expresses their behavior.
Reduction () is the binary relation defined by the rules below and closed under structural congruence; it specifies the computations that a process performs on its own.
[TABLE]
For the sake of generality, reduction allows dual endpoints with the same name to interact, independently of the domains of their subjects. The type system introduced next will ensure, among other things, local reductions, disallowing synchronisations among distinct domains.
3 Domain-aware Session Types via Hybrid Logic
This section develops a new domain-aware formulation of binary session types. Our system is based on a Curry-Howard interpretation of a linear variant of so-called hybrid logic, and can be seen as an extension of the interpretation of [9, 10] to hybrid (linear) logic. Hybrid logic is often used as an umbrella term for a class of logics that extend the expressiveness of propositional logic by considering modal worlds as syntactic objects that occur in propositions.
As in [9, 10], propositions are interpreted as session types of communication channels, proofs as typing derivations, and proof reduction as process communication. As main novelties, here we interpret: logical worlds as domains; the hybrid connective as the type of a session that migrates to an accessible domain ; and type-level quantification over worlds and as domain communication. We also consider a type-level operator (read “here”) which binds the current domain of the session to in . The syntax of domain-aware session types is given in Def. 3.1, where stand for domains drawn from , and where and are used as in the syntax of processes.
Definition 3.1** (Domain-aware Session Types).**
The syntax of types is defined by
[TABLE]
Types are the propositions of intuitionistic linear logic where the additives and are generalized to a labelled -ary variant. Propositions take the standard interpretation as session types, extended with hybrid logic operators [5], with worlds interpreted as domains that are explicitly subject to an accessibility relation (in the style of [45]) that is tracked by environment . Intuitively, is made up of direct accessibility hypotheses of the form , meaning that domain is accessible from .
Types are assigned to channel names; a type assignment enforces the use of name according to session , in the domain . A type environment is a collection of type assignments. Besides the accessibility environment just mentioned, our typing judgments consider two kinds of type environments: a linear part and an unrestricted part . They are subject to different structural properties: weakening and contraction principles hold for but not for . Empty environments are written as ‘’. We then consider two judgments:
[TABLE]
Judgment (i) states that can directly access under the hypotheses in . We write for the reflexive, transitive closure of , and when does not hold. Judgment (ii) states that process offers the session behavior specified by type on channel ; the session resides at domain , under the accessibility hypotheses , using unrestricted sessions in and linear sessions in . Note that each hypothesis in and is labeled with a specific domain. We omit when it is clear from context.
Typing Rules
Selected typing rules are given in Fig. 1; see [longversion] for the full listing. Right rules (marked with ) specify how to offer a session of a given type, left rules (marked with ) define how to use a session. The hybrid nature of the system induces a notion of well-formedness of sequents: a sequent is well-formed if for every , which we abbreviate as , meaning that all domains mentioned in are accessible from (not necessarily in a single direct step). No such domain requirement is imposed on . If an end sequent is well-formed, every sequent in its proof will also be well-formed. All rules (read bottom-up) preserve this invariant; only (), (), (), () and () require explicit checks, which we discuss below. This invariant statically excludes interaction between sessions in accessible domains (cf. Theorem 3.9).
We briefly discuss some of the typing rules, first noting that we consider processes modulo structural congruence; hence, typability is closed under by definition. Type denotes a session that inputs a session of type and proceeds as . To offer at domain , we input along that will offer at and proceed, now offering at :
[TABLE]
Dually, denotes a session that outputs a session that will offer and continue as . To offer , we output a fresh name with type along and proceed offering .
The () rule allows us to compose process , which offers , with process , which uses to offer . We require that domain is accessible from (i.e., ). We also require : the domains mentioned in (the context for ) must be accessible from , which follows from the transitive closure of the accessibility relation () using the intermediary domain . As in [9, 10], composition binds the name :
[TABLE]
Type means that no further interaction will take place on the session; names of type may be passed around as opaque values. types a session channel that offers its partner a choice between the behaviors, each uniquely identified by a label . Dually, types a session that selects some behavior by emitting the corresponding label. For flexibility and consistency with merge-based projectability in multiparty session types, rules for choice and selection induce a standard notion of session subtyping [25].
Type types a shared (non-linear) channel, to be used by a server for spawning an arbitrary number of new sessions (possibly none), each one conforming to type .
Following our previous remark on well-formed sequents, the only rules that appeal to accessibility are (), (), (), and (). These conditions are directly associated with varying degrees of flexibility in terms of typability, depending on what relationship is imposed between the domain to the left and to the right of the turnstile in the left rules. Notably, our system leverages the accessibility judgment to enforce that communication is only allowed between processes whose sessions are in (transitively) accessible domains.
The type operator realizes a domain migration mechanism which is specified both at the level of types and processes via name mobility tagged with a domain name. Thus, a channel typed with denotes that behavior is available by first moving to domain , directly accessible from the current domain. More precisely, we have:
[TABLE]
Hence, a process offering a behavior at ensures: (i) behavior is available at along a fresh session channel that is emitted along and (ii) is directly accessible from . To maintain well-formedness of the sequent we also must check that all domains in are still accessible from . Dually, using a service entails receiving a channel that will offer behavior at domain (and also allowing the usage of the fact that ).
Domain-quantified sessions introduce domains as fresh parameters to types: a particular service can be specified with the ability to refer to any existing directly accessible domain (via universal quantification) or to some a priori unspecified accessible domain:
[TABLE]
Rule () states that a process seeking to offer denotes a service that is located at domain but that may refer to any fresh domain directly accessible from in its specification (e.g. through the use of ). Operationally, this means that the process must be ready to receive from its client a reference to the domain being referred to in the type, which is bound to (occurring fresh in the typing derivation). Dually, Rule () indicates that a process interacting with a service of type must make concrete the domain that is directly accessible from it wishes to use, which is achieved by the appropriate output action. Rules () and () for the existential quantifier have a dual reading.
Finally, the type-level operator allows for a type to refer to its current domain:
[TABLE]
The typing rules that govern are completely symmetric and produce no action at the process level, merely instantiating the domain variable with the current domain of the session. As will be made clear in § 4, this connective plays a crucial role in ensuring the correctness of our analysis of multiparty domain-aware sessions in our logical setting.
By developing our type theory with an explicit domain accessibility judgment, we can consider the accessibility relation as a parameter of the framework. This allows changing accessibility relations and their properties without having to alter the entire system. To consider the simplest possible accessibility relation, the only defining rule for accessibility would be Rule () in Fig. 1. To consider an accessibility relation which is an equivalence relation we would add reflexivity, transitivity, and symmetry rules to the judgment.
Discussion and Examples
Being an interpretation of hybridized linear logic, our domain-aware theory is conservative wrt the Curry-Howard interpretation of session types in [9, 10], in the following sense: the system in [9, 10] corresponds to the case where every session resides at the same domain. As in [9, 10], the sequent calculus for the underlying (hybrid) linear logic can be recovered from our typing rules by erasing processes and name assignments.
Conversely, a fundamental consequence of our hybrid interpretation is that it refines the session type structure in non-trivial ways. By requiring that communication only occurs between sessions located at the same (or accessible) domain we effectively introduce a new layer of reasoning to session type systems. To illustrate this feature, consider the following session type , which specifies a simple interaction between a web store and its clients:
[TABLE]
allows clients to checkout their shopping carts by emitting a message or to . In the former case, the client pays for the purchase by sending their credit card data. If a banking service (not shown) approves the transaction (via an message), a receipt is emitted. Representable in existing session type systems (e.g. [9, 50, 30]), types and describe the intended communications but fail to capture the crucial fact that in practice the client’s sensitive information should only be requested after entering a secure domain. To address this limitation, we can use type-level domain migration to refine and :
[TABLE]
decrees that the interactions pertinent to type should be preceded by a migration step to the trusted domain , which should be directly accessible from ’s current domain. The type also specifies that the receipt must originate from a bank domain (e.g., ensuring that the receipt is never produced by the store without entering ). When considering the interactions with a client (at domain ) that checks out their cart, we reach a state that is typed with the following judgment:
[TABLE]
At this point, it is impossible for a (typed) client to interact with the behavior that is protected by the domain , since it is not the case that . That is, no judgment of the form is derivable.
This ensures, e.g., that a client cannot exploit the payment platform of the web store by accessing the trusted domain in unforeseen ways. The client can only communicate in the secure domain after the web store service has migrated accordingly, as shown by the judgment
[TABLE]
Technical Results
We state the main results of type safety via type preservation (Theorem 3.3) and global progress (Theorem 3.5). These results directly ensure session fidelity and deadlock-freedom. Typing also ensures termination, i.e., processes do not exhibit infinite reduction paths (Theorem 3.6). We note that in the presence of termination, our progress result ensures that communication actions are always guaranteed to take place. Moreover, as a property specific to domain-aware processes, we show domain preservation, i.e., processes respect their domain accessibility conditions (Theorem 3.9). The formal development of these results relies on a domain-aware labeled transition system [longversion], defined as a simple generalization of the early labelled transition system for the session -calculus given in [9, 10].
Type Safety and Termination. Following [9, 10], our proof of type preservation relies on a simulation between reductions in the session-typed -calculus and logical proof reductions.
Lemma 3.2** (Domain Substitution).**
Suppose . Then we have:
- •
*If then *
.
- •
* then *
.
Safe domain communication relies on domain substitution preserving typing (Lemma 3.2).
Theorem 3.3** (Type Preservation).**
*If and then
.*
Proof 3.4** (Proof (Sketch)).**
The proof mirrors those of [9, 10, 8, 46], relying on a series of lemmas relating the result of dual process actions (via our LTS semantics) with typable parallel compositions through the () rule [longversion]. For session type constructors of [9], the results are unchanged. For the domain-aware session type constructors, the development is identical that of [8] and [46], which deal with communication of types and data terms, respectively.
Following [9, 10], the proof of global progress relies on a notion of a live process, which intuitively consists of a process that has not yet fully carried out its ascribed session behavior, and thus is a parallel composition of processes where at least one is a non-replicated process, guarded by some action. Formally, we define if and only if , for some , names and a non-replicated guarded process .
Theorem 3.5** (Global Progress).**
If and then s.t. .
Note that Theorem 3.5 is without loss of generality since using the cut rules we can compose arbitrary well-typed processes together and need not occur in due to Rule ().
Termination (strong normalization) is a relevant property for interactive systems: while from a global perspective they are meant to run forever, at a local level participants should always react within a finite amount of time, and never engage into infinite internal behavior. We say that a process terminates, noted , if there is no infinite reduction path from .
Theorem 3.6** (Termination).**
If then .
Proof 3.7** (Proof (Sketch)).**
*By adapting the linear logical relations given in [40, 41, 8]. For the system in § 3 without quantifiers, the logical relations correspond to those in [40, 41], extended to carry over . When considering quantifiers, the logical relations resemble those proposed for polymorphic session types in [8], noting that no impredicativity concerns are involved. *
Domain Preservation. As a consequence of the hybrid nature of our system, well-typed processes are guaranteed not only to faithfully perform their prescribed behavior in a deadlock-free manner, but they also do so without breaking the constraints put in place on domain accessibility given by our well-formedness constraint on sequents.
Theorem 3.8**.**
Let be a derivation of . If is well-formed then every sub-derivation in well-formed.
While inaccessible domains can appear in , such channels can never be used and thus can not appear in a well-typed process due to the restriction on the rule. Combining Theorems 3.3 and 3.8 we can then show that even if a session in the environment changes domains, typing ensures that such a domain will be (transitively) accessible:
Theorem 3.9**.**
*Let (1) , (2) , and (3) . If then: (a) , for some ; (b) ; (c) . *
4 Domain-Aware Multiparty Session Types
We now shift our attention to multiparty session types [31]. We consider the standard ingredients: global types, local types, and the projection function that connects the two. Our global types include a new domain-aware construct, ; our local types exploit the hybrid session types from Def. 3.1. Rather than defining a separate type system based on local types for the process model of § 2, our analysis of multiparty protocols extends the approach defined in [7], which uses medium processes to characterize correct multiparty implementations. The advantages are twofold: on the one hand, medium processes provide a precise semantics for global types; on the other hand, they enable the principled transfer of the correctness properties established in § 3 for binary sessions (type preservation, global progress, termination, domain preservation) to the multiparty setting. Below, participants are ranged over by ; we write to denote a finite set of participants .
Besides the new domain-aware global type, our syntax of global types includes constructs from [31, 20]. We consider value passing in branching (cf. below), fully supporting delegation. To streamline the presentation, we consider global types without recursion.
Definition 4.1** (Global and Local Types).**
Define global types () and local types () as
[TABLE]
The completed global type is denoted . Given a finite and pairwise different labels, specifies that by choosing label , participant may send a message of type to participant , and then continue as . We decree , so reflexive interactions are disallowed. The global type specifies the migration of participants to domain in order to perform the sub-protocol ; this migration is lead by . Subsequently, all of migrate from back to their original domains and protocol is executed. This intuition will be made precise by the medium processes for global types (cf. Def. 4.8). Notice that and may involve different sets of participants. In writing we assume two natural conditions: (a) all migrating participants intervene in the sub-protocol (i.e., the set of participants of is exactly ) and (b) domain is accessible (via ) by all these migrating participants in . While subprotocols and session delegation may appear as similar, delegation supports a different idiom altogether, and has no support for domain awareness. Unlike delegation, with subprotocols we can specify a point where some of the participants perform a certain protocol within the same multiparty session and then return to the main session as an ensemble.
Definition 4.2**.**
The set of participants of (denoted ) is defined as: , , . We sometimes write to mean .
Global types are projected onto participants so as to obtain local types. The terminated local type is . The local type denotes an offer of a set of labeled alternatives; the local type denotes a behavior that chooses one of such alternatives. Exploiting the domain-aware framework in § 3, we introduce four new local types. They increase the expressiveness of standard local types by specifying universal and existential quantification over domains ( and ), migration to a specific domain (), and a reference to the current domain (, with occurring in ).
We now define (merge-based) projection for global types [20]. To this end, we rely on a merge operator on local types, which in our case considers messages .
Definition 4.3** (Merge).**
We define as the commutative partial operator on base and local types such that (and analogously for other base types), and
, where is one of the following: , , , , or ; 2. 2.
* *
\leavevmode\nobreak\ \qquad\mathtt{p}?\big{(}\{\mathit{l}_{k}\langle U_{k}\rangle.T_{k}\}_{k\in K\setminus J}\cup\{\mathit{l}^{\prime}_{j}\langle U^{\prime}_{j}\rangle.T^{\prime}_{j}\}_{j\in J\setminus K}\cup\{\mathit{l}_{l}\langle U_{l}\sqcup U^{\prime}_{l}\rangle.(T_{l}\sqcup T^{\prime}_{l})\}_{l\in K\cap J}\big{)}**
and is undefined otherwise.
Therefore, for to be defined there are two options: (a) and are identical base, terminated, selection, or “hybrid” local types; (b) and are branching types, but not necessarily identical: they may offer different options but with the condition that the behavior in labels occurring in both and must be mergeable.
To define projection and medium processes for the new global type , we require ways of “fusing” local types and processes. The intent is to capture in a single (sequential) specification the behavior of two distinct (sequential) specifications, i.e., those corresponding to protocols and . For local types, we have the following definition, which safely appends a local type to another:
Definition 4.4** (Local Type Fusion).**
The fusion of and , written , is given by:
[TABLE]
This way, e.g., if and , then . We can now define:
Definition 4.5** (Merge-based Projection [20]).**
Let be a global type. The merge-based projection of under participant , denoted , is defined as and
- •
\mathtt{p}\!\twoheadrightarrow\!\mathtt{q}{:}\{\mathit{l}_{i}\langle U_{i}\rangle.G_{i}\}_{i\in I}\!\!\upharpoonright\!{\mathtt{r}}={\small\begin{cases}\mathtt{p}!\{\mathit{l}_{i}\langle U_{i}\rangle.G_{i}\!\!\upharpoonright\!{\mathtt{r}}\}_{i\in I}&\text{if \mathtt{r}=\mathtt{p}}\\ \mathtt{p}?\{\mathit{l}_{i}\langle U_{i}\rangle.G_{i}\!\!\upharpoonright\!{\mathtt{r}}\}_{i\in I}&\text{if \mathtt{r}=\mathtt{q}}\\ \sqcup_{i\in I}\,G_{i}\!\!\upharpoonright\!{\mathtt{r}}&\text{otherwise (\sqcup as in Def.\leavevmode\nobreak\ \ref{d:mymerg})}\end{cases}}**
- •
(\mathtt{p}\,\mathsf{moves}\,\widetilde{\mathtt{q}}\,\mathsf{to}\,\omega\,\mathsf{for}\,G_{1}\,;\,G_{2})\!\!\upharpoonright\!{\mathtt{r}}={\small\begin{cases}\downarrow\!\beta.(\exists\alpha.@_{\alpha}\,G_{1}\!\!\upharpoonright\!{\mathtt{r}})\circ@_{\beta}\,G_{2}\!\!\upharpoonright\!{\mathtt{r}}&\text{if \mathtt{r}=\mathtt{p}}\\ \downarrow\!\beta.(\forall\alpha.@_{\alpha}\,G_{1}\!\!\upharpoonright\!{\mathtt{r}})\circ@_{\beta}\,G_{2}\!\!\upharpoonright\!{\mathtt{r}}&\text{if \mathtt{r}\in\widetilde{\mathtt{q}}}\\ G_{2}\!\!\upharpoonright\!{\mathtt{r}}&\text{otherwise}\end{cases}}**
When no side condition holds, the map is undefined.
The projection for the type is one of the key points in our analysis. The local type for , the leader of the migration, starts by binding the identity of its current domain (say, ) to . Then, the (fresh) domain is communicated, and there is a migration step to , which is where protocol will be performed. Finally, there is a migration step from back to ; once there, the protocol will be performed. The local type for all of follows accordingly: they expect from ; the migration from their original domains to (and back) is as for . For participants in , the fusion on local types (Def. 4.4) defines a local type that includes the actions for but also for , if any: a participant in need not be involved in . Interestingly, the resulting local types and define a precise combination of hybrid connectives whereby each migration step is bound by a quantifier or the current domain.
The following notion of well-formedness for global types is standard:
Definition 4.6** (Well-Formed Global Types [31]).**
We say that global type is well-formed (WF, in the following) if the projection is defined for all .
Analyzing Global Types via Medium Processes
A medium process is a well-typed process from § 2 that captures the communication behavior of the domain-aware global types of Def. 4.1. Here we define medium processes and establish two fundamental characterization results for them (Theorems 4.11 and 4.12). We shall consider names indexed by participants: given a name and a participant , we use to denote the name along which the session behavior of will be made available. This way, if then . To define mediums, we need to append or fuse sequential processes, just as Def. 4.4 fuses local types:
Definition 4.7** (Fusion of Processes).**
We define as the partial operator on well-typed processes such that (with ) :
[TABLE]
and is undefined otherwise.
The previous definition suffices to define a medium process (or simply medium), which uses indexed names to uniformly capture the behavior of a global type:
Definition 4.8** (Medium Process).**
Let be a global type (cf. Def. 4.1), be a set of indexed names, and a set of domains. The medium of , denoted , is defined as:
[TABLE]
where is as in Def. 4.7.
The medium for exploits four prefixes to mediate in the interaction between the implementations of and : the first two prefixes (on name ) capture the label selected by and the subsequently received value; the third and fourth prefixes (on name ) propagate the choice and forward the value sent by to . We omit the forwarding and value exchange when the interaction does not involve a value payload.
The medium for showcases the expressivity and convenience of our domain-aware process framework. In this case, the medium’s behavior takes place through the following steps: First, inputs a domain identifier (say, ) from which is forwarded to , the other participants of . Secondly, the roles migrate from their domains to . At this point, the medium for can execute, keeping track the current domain for all participants. Finally, the participants of migrate back to their original domains and the medium for executes.
Recalling the domain-aware global type of § 1, we produce its medium process:
[TABLE]
The medium ensures the client’s domain remains fixed through the entire interaction, regardless of whether the middleware chooses to interact with the server. This showcases how our medium transparently manages domain migration of participants.
Characterization Results
We state results that offer a sound and complete account of the relationship between: (i) a global type (and its local types), (ii) its medium process , and (iii) process implementations for the participants of . In a nutshell, these results say that the typeful composition of with processes for each (well-typed in the system of § 3) performs the intended global type. Crucially, these processes reside in distinct domains and can be independently developed, guided by their local type—they need not know about the medium’s existence or structure. The results generalize those in [7] to the domain-aware setting. Given a global type with , below we write to denote the set of indexed names . We define:
Definition 4.9** (Compositional Typing).**
We say is a compositional typing if: (i) it is a valid typing derivation; (ii) ; and (iii) .
A compositional typing says that depends on behaviors associated to each participant of ; it also specifies that does not offer any behaviors of its own.
The following definition relates binary session types and local types: the main difference is that the former do not mention participants. Below, ranges over base types ().
Definition 4.10** (Local TypesBinary Types).**
Mapping from local types (Def. 4.1) into binary types (Def. 3.1) is inductively defined as and
[TABLE]
Our first characterization result ensures that well-formedness of a global type guarantees the typability of its medium using binary session types. Hence, it ensures that multiparty protocols can be analyzed by composing the medium with independently obtained, well-typed implementations for each protocol participant. Crucially, the resulting well-typed process will inherit all correctness properties ensured by binary typability established in § 3.
Theorem 4.11** (Global Types Typed Mediums).**
If is WF with then is a compositional typing, for some , , with . We assume that for all (the medium’s domain is accessible by all), and that implies .
The second characterization result, given next, is the converse of Theorem 4.11: binary typability precisely delineates the interactions that underlie well-formed multiparty protocols. We need an auxiliary relation on local types, written , that relates types with branching and “here” type operators, which have silent process interpretations (cf. Figure 1 and [longversion]). First, we have if there is a such that (cf. Def. 4.3). Second, we have if (i) and and does not occur in ; but also if (ii) and T_{2}=T^{\prime}\{\raisebox{2.15277pt}{\small\omega}\!/\mbox{\small\alpha}\}. (See [longversion] for a formal definition of ).
Theorem 4.12** (Well-Typed Mediums Global Types).**
*Let be a global type (cf. Def. 4.1).
If is a compositional typing then such that and , for all .*
The above theorems offer a static guarantee that connects multiparty protocols and well-typed processes. They can be used to establish also dynamic guarantees relating the behavior of a global type and that of its associated set of multiparty systems (i.e., the typeful composition of with processes for each of ). These dynamic guarantees can be easily obtained by combining Theorems 4.11 and 4.12 with the approach in [7].
5 Related Work
There is a rich history of works on the logical foundations of concurrency (see, e.g., [4, 26, 1, 3]), which has been extended to session-based concurrency by Wadler [50], Dal Lago and Di Giamberardino [35], and others. Medium-based analyses of multiparty sessions were developed in [7] and used in an account of multiparty sessions in an extended classical linear logic [13].
Two salient calculi with distributed features are the Ambient calculus [15], in which processes move across ambients (abstractions of administrative domains), and the distributed -calculus (Dpi) [28], which extends the -calculus with flat locations, local communication, and process migration. While domains in our model may be read as locations, this is just one specific interpretation; they admit various alternative readings (e.g., administrative domains, security-related levels), leveraging the partial view of the domain hierarchy. Type systems for Ambient calculi such as [14, 6] enforce security and communication-oriented properties in terms of ambient movement but do not cover issues of structured interaction, central in our work. Garralda et al. [24] integrate binary sessions in an Ambient calculus, ensuring that session protocols are undisturbed by ambient mobility. In contrast, our type system ensures that both migration and communication are safe and, for the first time in such a setting, satisfy global progress (i.e., session protocols never jeopardize migration and vice-versa).
The multiparty sessions with nested protocols of Demangeon and Honda [18] include a nesting construct that is similar to our new global type , which also introduces nesting. The focus in [18] is on modularity in choreographic programming; domains nor domain migration are not addressed. The nested protocols in [18] can have local participants and may be parameterized on data from previous actions. We conjecture that our approach can accommodate local participants in a similar way. Data parameterization can be transposed to our logical setting via dependent session types [46, 49]. Asynchrony and recursive behaviors can also be integrated by exploiting existing logical foundations [22, 48].
Balzer et al. [2] overlay a notion of world and accessibility on a system of shared session types to ensure deadlock-freedom. Their work differs substantially from ours: they instantiate accessibility as a partial-order, equip sessions with multiple worlds and are not conservative wrt linear logic, being closer to partial-order-based typings for deadlock-freedom [34, 39].
6 Concluding Remarks
We developed a Curry-Howard interpretation of hybrid linear logic as domain-aware session types. Present in processes and types, domain-awareness can account for scenarios where domain information is only determined at runtime. The resulting type system features strong correctness properties for well-typed processes (session fidelity, global progress, termination). Moreover, by leveraging a parametric accessibility relation, it rules out processes that communicate with inaccessible domains, thus going beyond the scope of previous works.
As an application of our framework, we presented the first systematic study of domain-awareness in a multiparty setting, considering multiparty sessions with domain-aware migration and communication whose semantics is given by a typed (binary) medium process that orchestrates the multiparty protocol. Embedded in a fully distributed domain structure, our medium is shown to strongly encode domain-aware multiparty sessions; it naturally allows us to transpose the correctness properties of our logical development to the multiparty setting.
Our work opens up interesting avenues for future work. Mediums can be seen as monitors that enforce the specification of a domain-aware multiparty session. We plan to investigate contract-enforcing mediums building upon works such as [27, 32, 19], which study runtime monitoring in session-based systems. Our enforcement of communication across accessible domains suggests high-level similarities with information flow analyses in multiparty sessions (cf. [12, 11, 16]), but does not capture the directionality needed to model such analyses outright. It would be insightful to establish the precise relationship with such prior works.
Appendix A Appendix
A.1 Structural Congruence
Definition A.1**.**
Structural congruence* () is the least congruence relation on processes such that*
[TABLE]
A.2 Labeled Transition System
Some technical results rely on labeled transitions rather than on reduction. To characterize the interactions of a well-typed process with its environment, we extend the early labeled transition system (LTS) for the -calculus [44] with labels and transition rules for choice, migration, and forwarding constructs. A transition denotes that may evolve to by performing the action represented by label . Transition labels are defined below:
[TABLE]
Actions are name input , domain input , the offers and , migration and their matching co-actions, respectively the output and bound output actions, the domain output , label selections and , and domain migration . Both the bound output and migration action denote extrusion of a fresh name along . Internal action is denoted by . In general, an action requires a matching co-action in the environment to enable progress.
Definition A.2** (Labeled Transition System).**
The relation labeled transition () is defined by the rules in Fig. 2, subject to the side conditions: in rule , we require ; in rule , we require ; in rule , we require . We omit the symmetric versions of rules , , and .
We write for the subject of the action , that is, the channel along which the action takes place. Weak transitions are defined as usual. Let us write for the composition of relations and for the reflexive, transitive closure of . Notation stands for (given ) and stands for . We recall basic facts about reduction, structural congruence, and labeled transition: closure of labeled transitions under structural congruence, and coincidence of -labeled transition and reduction [44]: (1) if then ; (2) iff .
A.3 Omitted Typing Rules
[TABLE]
A.4 Additional Lemmas for Type Preservation
The development of type preservation extends that of [9] to account for domain communication and migration. The proof mainly relies on a series of reduction lemmas (one per session type connective that produces observable process actions) that relate process actions with parallel composition through the () rule, which correspond to logical proof reductions. For instance, the reduction lemma for is:
Lemma A.3** (Reduction Lemma – ).**
*Assume
(a) with ; and
(b) with .
Then: *
These lemmas carry over straightforwardly from [9]. The new lemmas are:
Lemma A.4** (Reduction Lemma - ).**
*Assume
(a) with and
(b) with .
Then: *
Lemma A.5** (Reduction Lemma - ).**
*Assume
(a) with and
(b) with .
Then: *
Lemma A.6** (Reduction Lemma - ).**
*Assume
(a) with and
(b) with .
Then: *
The proofs of the lemmas above follow by simultaneous induction on the two given typing derivations, with Lemmas A.4 and A.5 making use of Lemma 3.2. This development is essentially that of [8] and [46] which consider an extension of the core propositional system of [9] with communication of types (i.e. polymorphism) and communication of data (i.e. value dependencies). By appealing to such lemmas, we can establish type preservation for our system.
A.5 Pre-congruence on Local Types
The following definition is used in the proof of Thm. 4.12:
Definition A.7**.**
We define as the least pre-congruence relation on local types such that
[TABLE]
A.6 Proofs of Medium Characterization
The proof of Theorem 4.11 relies on the following auxiliary proposition:
Proposition A.8**.**
Let
, with 2. 2.
**
be two compositional typings. Then
[TABLE]
is a compositional typing, where the typing environment is defined as follows:
[TABLE]
Proof A.9** (Proof (Sketch)).**
We must prove the existence of a typing derivation for the resulting fused process. We start by observing that the compositional typing for ensures that its associated derivation will contain one or more occurrences of the sequent
[TABLE]
corresponding to one or more occurrences of in (possible because of labeled choices in ): indeed, by Def. 4.8 we have and by Def. 4.10 we have . Observe that the compositional typing for
[TABLE]
ensures that , i.e., contains judgements for at least the names in —it may also contain other judgments, corresponding to participants that intervene in but not in the sub-protocol . Given this, the compositional typing for the fused process
[TABLE]
is obtained by “stacking up” the typing derivation for (2) exactly on the occurrences of sequents of the form (1) in the typing derivation for . This is fully consistent with definitions of fusion for processes (Def. 4.7) and local types (Def. 4.4): the former decrees that whereas the latter decrees that . In the resulting “stacked” typing derivation, the types for that correspond to the behavior of can be derived exactly as in the derivation of the first assumption, now starting from the types rather than from .
See 4.11
Proof A.10**.**
By induction on the structure of . There are three cases.
- •
The base case, , is immediate as there are no participants.
- •
The case is exactly as in **[7]**, but we report it here for the sake of completeness. By the well-formedness assumption (Def. 4.6), local types are all defined. Writing and instead of and , by Def. 4.5 we have:
[TABLE]
We need to show that, for some and ,
[TABLE]
is a compositional typing, with .
Without loss of generality, we detail the case . By Def. 4.8, we have:
[TABLE]
and by combining (3) and (4) with Def. 4.10 we have:
[TABLE]
Now, by assumption is WF; then, by construction, both and are WF too. Therefore, by using IH twice we may infer that both
[TABLE]
are compositional typings, for any and , with
[TABLE]
Now, to obtain a compositional typing for , we must consider that and may not be identical. This is due to the merge-based well-formedness assumption, which admits non identical behaviors in branches and in the case of (local) branching types (cf. Def. 4.3).
We proceed by induction on , defined as the size of and (note that ).
(Case ): Then and and are the only participants in . Let us write to stand for the session type
[TABLE]
Based on (7) and (8), following the derivation in Fig. 3, we may derive typings
[TABLE]
The proof for this case is completed using (9) and (10) as premises for Rule ():
[TABLE]
(Case ): Then there exists a participant , types , and environments such that and .
By induction hypothesis, there is a compositional typing starting from
[TABLE]
resulting into
[TABLE]
since .
To extend the typing derivation to and , we proceed by a case analysis on the shape of and . We aim to show that either (a) and are already identical base or session types or (b) that typing allows us to transform them into identical types. We rely on the definition of (Def. 4.3). There are two main sub-cases:
- (a)
Case : Then, since Def. 4.3 decrees and the fact that merge-based well-definedness depends on , we may infer . Hence, and the desired derivation is obtained as in the base case. 2. (b)
Case : This is the interesting case: even if merge-based well-formedness of ensures that both and are selection types, they may not be identical. If and are identical then we proceed as in previous sub cases. Otherwise, then due to there are some finite number of labeled alternatives in but not in and/or viceversa. Also, Def. 4.3 ensures that common options (if any) are identical in both branches. We may then use Rule () (cf. Appendix A.3) to “complement” occurrences of types and in (7) and (8) as appropriate to make them coincide and achieve identical typing. Rule () is silent; as labels are finite, this completing task is also finite, and results into .
- •
Finally, we have the case . Without loss of generality, we consider the global type , i.e., the type in which the sub-protocol only involves two participants, namely and . By the well-formedness assumption, local types , , are all defined. In particular, by Def. 4.5 we have:
[TABLE]
We need to show that, for some ,
[TABLE]
with \Delta\{\raisebox{2.15277pt}{\small\tilde{c}}\!/\mbox{\small\tilde{m}}\}=c_{\mathtt{p}_{3}}{:}\langle\!\langle G\!\!\upharpoonright\!{\mathtt{p}_{3}}\rangle\!\rangle[\omega_{3}],\leavevmode\nobreak\ \ldots,\leavevmode\nobreak\ c_{\mathtt{p}_{n}}{:}\langle\!\langle G\!\!\upharpoonright\!{\mathtt{p}_{n}}\rangle\!\rangle[\omega_{n}] is a compositional typing. By Def. 4.8, we have:
[TABLE]
and by combining (11) and (12) with Def. 4.10 we have:
[TABLE]
Now, by assumption is WF; then, by construction both and are WF too. Therefore, by using IH twice we may infer that both
[TABLE]
are compositional typings, for any , , with as above. Using Rule () twice, assuming and , from (16) we can derive:
[TABLE]
Using Prop. A.8 on (15) and (17) we obtain:
[TABLE]
We then have the following derivation, which completes the proof for this case:
[TABLE]
The proof of the converse of Thm. 4.11 proceeds similarly; we must take into account that, given a global type , the process structure of will induce types closely related to , up to occurrences of two type operators whose typing rules enforce a silent interpretation of processes, namely () and ().
See 4.12
Proof A.11** (Proof (Sketch)).**
By induction on the structure of , following the lines of the proof of Thm. 4.11, exploiting (cf. Def. A.7). There are three cases:
- •
(Case ): Then , , and the thesis follows vacuously. Notice that from the assumption and Rule () we may derive
[TABLE]
for any . In that case, observe that Def. 4.5 decrees that , for any . There could be spurious occurrences of “here”, as in, e.g,, . The thesis holds using , for (cf. Def. 4.10).
- •
(Case ) This case follows by typing inversion on the structure of , using the derivation presented in the second case of the proof of Thm. 4.11. The main aspect to consider are the possible uses of the silent Rule (): to prove the correspondence between and the branching type , we exploit the first axiom of (cf. Def. A.7) to appropriately handle/prune silently added alternatives in the branching. We use to relate and up to occurrences of “here” as above.
- •
(Case ) This case also follows by typing inversion on the structure of , using the derivation presented in the third case of the proof of Thm. 4.11. The main aspect to consider for the intended correspondence is that Rule () silently induces type constructs of the form within the types for . To obtain the correspondence, we exploit the second and third axioms of , which make explicit required “here” operators in the type and remove spurious “heres”, respectively.
Appendix B Extended Examples
B.1 Negotiation Procedure
This example is adapted from [18], consisting of a negotiation procedure Nego between two participants of a three-party interaction. The negotiation consists of an agreement on a contract: one participant specifies a request, while the other offers a corresponding contract. The first participant may either accept the contract and end the protocol or make a counter-offer. For the sake of conciseness we assume that the counter-offer is accepted:
[TABLE]
The main protocol consists of a client, an agent and an instrument, each initially in their own domains. The client first sends a request to the agent for some instrument they wish to use. The agent connects to the instrument which acknowledges when available. The agent then enters the negotiation sub-protocol with the client (via protocol ), by having both agent and the client migrate to domain . This movement models the trusted setting at which the agent and the client coexist in order to successfully negotiate the instrument usage. After the negotiation stage is complete, both the client and the instrument migrate to a common domain to perform the rest of the protocol, which for the sake of conciseness we model with the client either aborting the interaction or sending a command to the instrument and then receiving back the appropriate result:
[TABLE]
By leveraging our notion of medium, we can make explicit the fact that the three participants are distributed agents, each located at independent domains that can access the medium substrate (i.e. the domain of the medium). Through the medium-orchestrated interaction, the use of domain migration primitives enables us to explicitly model the various domain movement steps that the participants must follow to implement the protocol. This is in sharp contrast with more traditional approaches to multiparty protocols [31], where such domain specific notions are implicit. The medium for the global type above is (we assume that the three participants initially reside at worlds , respectively):
[TABLE]
The first two lines of the medium definition correspond to the initial exchange between the client, the agent and the instrument. The actions after the emission of label to the client model the migration protocol: the agent emits the domain identifier to the medium, which then forwards it to the client and receives from both participants the session handles and , located at . After the migration takes place, the medium orchestrates the negotation between the agent and the client using the new session handles.
After the negotiation, the agent and the client migrate back to their initial domains and , respectively, and the interactions between the client and the instrument take place: the client and the instrument migrate to , sending to the medium the session handles and , followed by the client emitting an or message which is forwarded to the instrument. In the latter case, the instrument forwards the result to the client. Finally, both the client and the instrument migrate back to their initial domains.
B.2 Domain-aware Middleware
A common design pattern in distributed computing is the notion of a middleware agent which answers requests from clients, sometimes offloading the requests to some server (e.g. to better manage local resource availability). The mediation between the middleware and the server often involves some form of privilege escalation or specialized authentication, which we can now model via domain migration. We first represent a simple offloading protocol between the middleware and the server :
[TABLE]
The global interaction is represented by the following global type:
[TABLE]
The medium for this protocol is given by:
[TABLE]
Notice how the client’s domain remains fixed throughout the entire interaction, regardless of whether or not the middleware chooses to interact with the server to fulfil the client request.
B.3 A Secure Communication Domain
Our previous examples explore the use of domains in a general distributed setting. Another interesting aspect of our domain-aware typing discipline is that communication can only take place between accessible domains. In scenarios where participants are each situated in distinct domains, domain movement also governs the ability of participants to interact. For instance, consider the following protocol excerpt:
[TABLE]
The protocol above is part of the interaction between an online store and its clients, where after some number of exchanges the client decides to purchase the contents of their shopping cart. Upon receiving the message, the store is meant to enter a secure domain so it can communicate with the bank role to exchange potentially sensitive data. In a setting where the client, store and bank exist at different domains and where only the store domain can access the bank domain, our domain-aware typing discipline ensures that no direct communication between the bank and the client domain is possible, with the entirety of the data flows between the client and the bank (via the medium) being captured by the type and medium specification.
Appendix C Examples of Domain-aware Binary Sessions
In this section we present two examples that further illustrate the novel features of our domain-aware framework for session communications.
C.1 E-Commerce Example
We revisit the web store example of § 3. Recall the refined web store session type:
[TABLE]
The process that implements the bank interface is to be accessible from the domain of the web store, moving to a secure domain before receiving and validating the payment information. Thus, the bank process typing can be specified with the following judgment, recalling that the domain of the web store is :
[TABLE]
The web store will then use the bank interface to fulfill its interface:
[TABLE]
The type constructor allows us to express a very precise form of coordinated domain migration. For instance, typing ensures that in order for the store to produce an output of the form it must first have interacted with the bank domain: in order to produce an output of , it must be the case that , which is only known to the store process after interacting with the bank domain. Alternatively, consider the service interacting with a client process along channel , each in their own (accessible) domains, and , respectively. Our framework ensures that interactions between the client and the web store enjoy session fidelity, progress, and termination guarantees. Concerning domain-awareness, by assuming the client chooses to buy his product selection, we reach a state that is typed as follows:
[TABLE]
At this point, it is impossible for a (typed) client to interact with the behavior that is protected by the trusted domain , since it is not the case that . This ensures, e.g., that a client cannot exploit the payment platform of the web store by accessing the trusted domain in unforeseen ways. Formally, no typing derivation of exists (Theorem 3.8). The client can only communicate in the secure domain after the web store service has migrated accordingly:
[TABLE]
It is inconvenient (and potentially error-prone) for the payment domain to be hardwired in the type. We can solve this issue via existential quantification as shown in the introduction.
[TABLE]
As long as accessibility is irreflexive and antisymmetric, the server-provided payment domain will not be able to interact with the initial domain of the interaction except as specified in the type.
Alternatively, the server can let the client choose a payment domain by using universal quantification. Compliant server code will only be able to communicate in the client-provided payment domain since the process must be parametric in .
[TABLE]
C.2 Spatial Distribution as in 5
Murphy et al. [38] have proposed a Curry-Howard interpretation of the intuitionistic modal logic S5 [45] to model distributed computation with worlds as explicit loci for computation. Accessibility between worlds was assumed to be reflexive, transitive, and symmetric because each host on a network should be accessible from any other host. Murphy [37] later generalized this to hybrid logic, an idea also present in [33], so that propositions can explicitly refer to worlds. Computation in this model was decidedly sequential, and a concurrent extension was proposed as future work. Moreover, the system presented some difficulties in the presence of disjunction, requiring a so-called action at a distance without an explicit communication visible in the elimination rule for disjunction.
The present system not only generalizes to permit concurrency through session-typed linearity, but also solves the problem of action at a distance because all communication is explicit in the processes. Due to this issue in the original formulation of , we will not attempt here to give a full, computationally adequate interpretation of in our system (which would generalize [47]), but instead explain the spatially distributed computational interpretation of our type system directly.
. Channel offering can be used in any domain. 2.
. Channel is offering in some (hidden) domain.
These are mapped into our hybridized linear logic (choosing a fresh each time) with
[TABLE]
A process will therefore receive, along , a world accessible from and then move to , offering in domain . Conversely, a process will send a world along and then move to , offering in domain . Processes using such channels will behave dually.
We can now understand the computational interpretation of some of the distinctive axioms of S5, keeping in mind that accessibility should be reflexive, transitive, and symmetric (we make no distinction between direct accessibility or accessibility requiring multiple hops).
.
Here, is offered along some at some unknown domain accessible from . Move the offer of to as and send it to obtain . We abstract this as , which is possible since . Intuitively, this axiom captures the fact that a session transformer that can be used in any domain may be combined with a session offered in some domain to produce a session behavior , itself in some hidden domain.
[TABLE] 2.
.
Given a session that offers at , we offer at by appealing to reflexivity, and thus . This means that we can then receive from a fresh channel , obtaining an ambient session of type at domain which we then forward along . The axiom captures the fact that a mobile session can in fact be accessed “anywhere”.
[TABLE] 3.
Given a session offering at , this means that is offering the behavior at some accessible but unknown domain . We can use this session to provide somewhat of a “link” session, that allows any other domain to also access the behavior at this accessible, unknown, domain. We do this by first receiving along , identifying the domain accessible from which we wish to link to . We then send along the fresh session located at , along which we shall provide the connection. We may then receive from the identity of and a session located in this domain, send the identity along and a fresh session , located at (only possible due to the accessibility relation being an equivalence) which we then forward from as needed.
[TABLE]
Other axioms can be given similarly straightforward interpretations and process realizations.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Samson Abramsky. Computational interpretations of linear logic. Theor. Comput. Sci. , 111(1&2):3–57, 1993. URL: https://doi.org/10.1016/0304-3975(93)90181-R , doi:10.1016/0304-3975(93)90181-R . · doi ↗
- 2[2] Stephanie Balzer, Bernardo Toninho, and Frank Pfenning. Manifest deadlock-freedom for shared session types. In Programming Languages and Systems - 28th European Symposium on Programming, ESOP 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings , pages 611–639, 2019.
- 3[3] Emmanuel Beffara. A concurrent model for linear logic. Electr. Notes Theor. Comput. Sci. , 155:147–168, 2006. URL: https://doi.org/10.1016/j.entcs.2005.11.055 , doi:10.1016/j.entcs.2005.11.055 . · doi ↗
- 4[4] Gianluigi Bellin and Philip J. Scott. On the pi-calculus and linear logic. Theor. Comput. Sci. , 135(1):11–65, 1994. URL: https://doi.org/10.1016/0304-3975(94)00104-9 , doi:10.1016/0304-3975(94)00104-9 . · doi ↗
- 5[5] Torben Braüner and Valeria de Paiva. Intuitionistic hybrid logic. J. of App. Log. , 4:231–255, 2006.
- 6[6] Michele Bugliesi and Giuseppe Castagna. Behavioural typing for safe ambients. Comput. Lang. , 28(1):61–99, 2002.
- 7[7] Luís Caires and Jorge A. Pérez. Multiparty session types within a canonical binary theory, and beyond. In Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, Held as Part of the 11th International Federated Conference on Distributed Computing Techniques, Dis Co Tec 2016, Heraklion, Crete, Greece, June 6-9, 2016, Proceedings , pages 74–95, 2016. Extended version with proofs at https://sites.google.com/a/jor
- 8[8] Luís Caires, Jorge A. Pérez, Frank Pfenning, and Bernardo Toninho. Behavioral polymorphism and parametricity in session-based communication. In ESOP , volume 7792 of LNCS . Springer, 2013.