Marco Carbone

LOPSTR Conference 2023 Conference Paper

A Logical Interpretation of Asynchronous Multiparty Compatibility

• Marco Carbone
• Sonia Marin
• Carsten Schürmann 0001

Abstract Session types specify the protocols that communicating processes must follow in a concurrent system. When composing two or more processes, a session typing system must check whether such processes are compatible, i. e. , that all sent messages are eventually received and no deadlock ever occurs. After the propositions-as-types paradigm, relating session types to linear logic, previous work has shown that duality, in the binary case, and more generally coherence, in the multiparty case, are sufficient syntactic conditions to guarantee compatibility for two or more processes, yet do not characterise all compatible set of processes. In this work, we generalise duality/coherence to a notion of forwarder compatibility. Forwarders are specified as a restricted family of proofs in linear logic, therefore defining a specific set of processes that can act as middleware by transfering messages without using them. As such, they can guide a network of processes to execute asynchronously. Our main result establishes forwarder compatibility as a sufficient and necessary condition to fully capture all well-typed multiparty compatible processes.

LOPSTR Conference 2018 Conference Paper

Multiparty Classical Choreographies

• Marco Carbone
• Luís Cruz-Filipe
• Fabrizio Montesi
• Agata Murawska

Abstract We present Multiparty Classical Choreographies (MCC), a language model where global descriptions of communicating systems (choreographies) implement typed multiparty sessions. Typing is achieved by generalising classical linear logic to judgements that explicitly record parallelism by means of hypersequents. Our approach unifies different lines of work on choreographies and processes with multiparty sessions, as well as their connection to linear logic. Thus, results developed in one context are carried over to the others. Key novelties of MCC include support for server invocation in choreographies, as well as logic-driven compilation of choreographies with replicated processes.

TCS Journal 2018 Journal Article

On the boundary between decidability and undecidability of asynchronous session subtyping

• Mario Bravetti
• Marco Carbone
• Gianluigi Zavattaro

Session types are behavioural types for guaranteeing that concurrent programs are free from basic communication errors. Recent work has shown that asynchronous session subtyping is undecidable. However, since session types have become popular in mainstream programming languages in which asynchronous communication is the norm rather than the exception, it is crucial to detect significant decidable subtyping relations. Previous work considered extremely restrictive fragments in which limitations were imposed to the size of communication buffer (at most 1) or to the possibility to express multiple choices (disallowing them completely in one of the compared types). In this work, for the first time, we show decidability of a fragment that does not impose any limitation on communication buffers and allows both the compared types to include multiple choices for either input or output, thus yielding a fragment which is more significant from an applicability viewpoint. In general, we study the boundary between decidability and undecidability by considering several fragments of subtyping. Notably, we show that subtyping remains undecidable even if restricted to not using output covariance and input contravariance.

I&C Journal 2017 Journal Article

Undecidability of asynchronous session subtyping

• Mario Bravetti
• Marco Carbone
• Gianluigi Zavattaro

Session types are used to describe communication protocols in distributed systems and, as usual in type theories, session subtyping characterizes substitutability of the communicating processes. We investigate the (un)decidability of subtyping for session types in asynchronously communicating systems. We first devise a core undecidable subtyping relation that is obtained by imposing limitations on the structure of types. Then, as a consequence of this initial undecidability result, we show that (differently from what stated or conjectured in the literature) the three notions of asynchronous subtyping defined so far for session types are all undecidable. Namely, we consider the asynchronous session subtyping by Mostrous and Yoshida for binary sessions, the relation by Chen et al. for binary sessions under the assumption that every message emitted is eventually consumed, and the one by Mostrous et al. for multiparty session types. Finally, by showing that two fragments of the core subtyping relation are decidable, we evince that further restrictions on the structure of types make our core subtyping relation decidable.

TCS Journal 2009 Journal Article

Foreword: Festschrift for Mogens Nielsen’s 60th birthday

• Marco Carbone
• Paweł Sobociński
• Frank D. Valencia