Related papers: Forwarders as Process Compatibility, Logically

Session types have been proposed as a means of statically verifying implementations of communication protocols. Although prior work has been successful in verifying some classes of protocols, it does not cope well with parameterized,…

Global types are formal specifications that describe communication protocols in terms of their global interactions. We present a new, streamlined language of global types equipped with a trace-based semantics and whose features and…

We provide the first denotational semantics for asynchronous multiparty session types with precise asynchronous subtyping. Our semantics enables us to reason about asynchronous message-passing, in which message-sending is non-blocking. It…

Information flow control type systems statically restrict the propagation of sensitive data to ensure end-to-end confidentiality. The property to be shown is noninterference, asserting that an attacker cannot infer any secrets from made…

Formal verification methods for concurrent systems cannot always be scaled-down or tailored in order to be applied on specific subsystems. We address such an issue in a MultiParty Session Types setting by devising a partial type assignment…

One way to interpret the reasoning power of transformer-based language models is to describe the types of logical rules they can resolve over some input text. Recently, Chiang et al. (2023) showed that finite-precision transformers can be…

Session types provide guarantees about concurrent behaviour and can be understood through their correspondence with linear logic, with propositions as sessions and proofs as processes. However, a strictly linear setting is somewhat…

Sessions are a fundamental notion in message-passing systems. A session is an abstract notion of communication between parties where each one owns an endpoint. Session types are types that are assigned to the endpoints and that are used to…

Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms, and recent years have seen a number of proposals of program logics for proving it. Although these logics differ in technical details, they…

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…

While formal models of concurrency tend to focus on synchronous communication, asynchronous communication is relevant in practice. In this paper, we will discuss asynchronous communication in the context of session-based concurrency, the…

We tackle the problem of statically ensuring that message-passing programs never run into deadlocks. We focus on concurrent functional programs governed by context-free session types, which can express rich tree-like structures not…

Message-passing software systems exhibit non-trivial forms of concurrency and distribution; they are expected to follow intended protocols among communicating services, but also to never "get stuck". This intuitive requirement has been…

We propose an interpretation of multiparty sessions as "flow event structures", which allows concurrency between communications within a session to be explicitly represented. We show that this interpretation is equivalent, when the…

This paper elaborates on a new approach of the question of the proof-theoretic study of concurrent interaction called "proofs as schedules". Observing that proof theory is well suited to the description of confluent systems while…

Initiated by Abramsky [1994], the Proofs as Processes agenda is to establish a solid foundation for the study of concurrent languages, by researching the connection between linear logic and the $\pi$-calculus. To date, Proofs as Processes…

The additional complexity caused by concurrently communicating processes in distributed systems render the verification of such systems into a very hard problem. Multiparty session types were developed to govern communication and…

The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this…

Behavioural type systems ensure more than the usual safety guarantees of static analysis. They are based on the idea of "types-as-processes", providing dedicated type algebras for particular properties, ranging from protocol compatibility…

Prior work has extended the deep, logical connection between the linear sequent calculus and session-typed message-passing concurrent computation with equi-recursive types and a natural notion of subtyping. In this paper, we extend this…