Session types and subtyping for orchestrated interactions (Q1633346)

This paper is an extended version of a presentation given at Interaction and Concurrency Experience 2017 [the authors, Electron. Proc. Theor. Comput. Sci. (EPTCS) 261, 17--36 (2017; Zbl 1432.68300)]. When a client interacts with a server, the options (e.g., methods of payment) accepted by the client can differ from the options offered by the server. When the intersection of the acceptable options and of the offered options is non-empty, it is natural to expect the transaction to succeed. Unfortunately, this simple observation could not be represented in the formal system of session types, and this paper offers a way of bridging that gap. There are multiple type systems for (variations of) concurrent systems, but quite often they rely on the logical notion of duality to present their formalism, and of compliance to capture processes such that every action of one can be matched by a co-action of the other. From my point of view, the two main contributions of this paper are to 1) introduce a new operator that does not have a dual, and that models ``accepting one of the following options'', and 2) to relax the notion of compliance for type sessions. Orchestrated and retractable compliances were born in the theory of contracts, but never adapted to session types. The first kind adds an orchestrator between processes whenever they open a channel that ensures that the exchanges will lead to an agreement. The technicalities of adapting this formalism to type sessions is detailed and carried out very competently by the authors. Among other results, typable processes are proven free of particular errors, and a sub-typing routine is defined. Some of the explanations could have benefitted from a better writing, but the numerous examples and intuitions allow for an easy reading. The relaxed notion of compliance is of real interest, and could lead to notable progress in the specification and testing of distributed services. Some of the formalism ends up being quite heavy, but with the help of the detailed explanations and guidance of the authors (for instance, when they present their operational semantics rule by rule) readers will not miss the important details.