Related papers: Session Types for Orchestrated Interactions
This work proposes a dependent type theory that combines functions and session-typed processes (with value dependencies) through a contextual monad, internalising typed processes in a dependently-typed lambda-calculus. The proposed…
We present an asynchronous calculus for multiparty sessions with mixed choice, which extends the Simple MultiParty Session framework in order to support nondeterministic choices with both input and output prefixes. Global types -- equipped…
Session types have emerged as a typing discipline for communication protocols. Existing calculi with session types come equipped with many different primitives that combine communication with the introduction or elimination of the…
Much research has studied foundations for correct and reliable communication-centric systems. A salient approach to correctness uses session types to enforce structured communications; a recent approach to reliability uses reversible…
In calculi for modelling communication protocols, internal and external choices play dual roles. Two external choices can be viewed naturally as dual too, as they represent an agreement between the communicating parties. If the interaction…
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type…
Session types statically prescribe bidirectional communication protocols for message-passing processes and are in a Curry-Howard correspondence with linear logic propositions. However, simple session types cannot specify properties beyond…
Session types are a discipline for the static verification of message-passing programs. A session type specifies a channel's protocol as sequences of exchanges. It is most relevant to investigate session-based concurrency by identifying the…
A multiparty session formalises a set of concurrent communicating participants. We propose a type system for multiparty sessions where some communications between participants can be ignored. This allows us to type some sessions with global…
Session type systems have been given logical foundations via Curry-Howard correspondences based on both intuitionistic and classical linear logic. The type systems derived from the two logics enforce communication correctness on the same…
The classes of depth-bounded and name-bounded processes are fragments of the pi-calculus for which some of the decision problems that are undecidable for the full calculus become decidable. P is depth-bounded at level k if every reduction…
Programs are more distributed and concurrent today than ever before, and structural communications are at the core. Constructing and debugging such programs are hard due to the lack of formal specification/verification of concurrency. This…
In recent work, we have developed a session types discipline for a calculus that features the usual constructs for session establishment and communication, but also two novel constructs that enable communicating processes to be stopped,…
Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication…
Imperative session types provide an imperative interface to session-typed communication. In such an interface, channel references are first-class objects with operations that change the typestate of the channel. Compared to functional…
Multiparty session types (MPST) are a robust typing framework that ensures safe and deadlock-free communication within distributed protocols. As these protocols grow in complexity, compositional modelling becomes increasingly important to…
MultiParty Session Types (MPST) provide a useful framework for safe concurrent systems. Mixed choice (enabling a participant to play at the same time the roles of sender and receiver) increases the expressive power of MPST as well as the…
Session types statically prescribe bidirectional communication protocols for message-passing processes. However, simple session types cannot specify properties beyond the type of exchanged messages. In this paper we extend the type system…
Session types are a typed approach to message-passing concurrency, where types describe sequences of intended exchanges over channels. Session type systems have been given strong logical foundations via Curry-Howard correspondences with…
Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or…