Related papers: Undecidability of Asynchronous Session Subtyping
In programming models with a reversible semantics, computational steps can be undone. This paper addresses the integration of reversible semantics into process languages for communication-centric systems equipped with behavioral types. In…
We present the first session typing system guaranteeing request-response liveness properties for possibly non-terminating communicating processes. The types augment the branch and select types of the standard binary session types with a set…
In the setting of the pi-calculus with binary sessions, we aim at relaxing the notion of duality of session types by the concept of retractable compliance developed in contract theory. This leads to extending session types with a new type…
Multiparty session types are designed to abstractly capture the structure of communication protocols and verify behavioural properties. One important such property is progress, i.e., the absence of deadlock. Distributed algorithms often…
There has been a considerable amount of work on retrieving functions in function libraries using their type as search key. The availability of rich component specifications, in the form of behavioral types, enables similar queries where one…
Regular synchronization languages can be used to define rational relations of finite words, and to characterize subclasses of rational relations, like automatic or recognizable relations. We provide a systematic study of the decidability of…
To celebrate the 30th edition of EXPRESS and the 20th edition of SOS we overview how session types can be expressed in a type theory for the standard $\pi$-calculus by means of a suitable encoding. The encoding allows one to reuse results…
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…
We show that the first-order theory of structural subtyping of non-recursive types is decidable. Let $\Sigma$ be a language consisting of function symbols (representing type constructors) and $C$ a decidable structure in the relational…
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…
This paper presents the first implementation of session types in a dynamically-typed language - Python. Communication safety of the whole system is guaranteed at runtime by monitors that check the execution traces comply with an associated…
Conversation disentanglement aims to separate intermingled messages into detached sessions, which is a fundamental task in understanding multi-party conversations. Existing work on conversation disentanglement relies heavily upon…
We formulate a model for intermittent communication that can capture bursty transmissions or a sporadically available channel, where in either case the receiver does not know a priori when the transmissions will occur. Focusing on the…
Planning is one of the most studied problems in computer science. In this paper, we consider the timeline-based approach, where the domain is modeled by a set of independent, but interacting, components, identified by a set of state…
Consensus is one of the most fundamental problems in distributed computing. This paper studies the consensus problem in a synchronous dynamic directed network, in which communication is controlled by an oblivious message adversary. The…
Multiparty session types (MST) are a well-established type theory that describes the interactive structure of a fixed number of components from a global point of view and type-checks the components through projection of the global type onto…
Mixed-choice has long been barred from models of asynchronous communication since it compromises key properties of communicating finite-state machines. Session types inherit this restriction, which precludes them from fully modelling…
We study the problem of parametric parallel complexity analysis of concurrent, message-passing programs. To make the analysis local and compositional, it is based on a conservative extension of binary session types, which structure the type…
Classic distributed control problems have an interesting dichotomy: they are either trivial or undecidable. If we allow the controllers to fully synchronize, then synthesis is trivial. In this case, controllers can effectively act as a…
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…