arXiv subjects

Franco Barbanera

Publications and source records attributed to Franco Barbanera.

At least 19 recordsLinked to original sources

arXiv2026

Asynchronous Multiparty Sessions with Mixed Choice

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 with a coinductively defined labelled transition system -- form the basis of a type system that exploits the key notion of coherence of communication label sets. Roughly, a coherent set contains either all the communications enabled in the session, or all the actions currently exhibited by a participant, provided that at least one input is enabled for each expected sender. Our approach to the typing of multiparty sessions is orthogonal to the well-established, projection-based approaches of the MultiParty Session Type framework. We prove fundamental theorems for typable multiparty sessions, including Subject Reduction and Session Fidelity. These properties imply that typable sessions are both Lock-Free and Orphan-Message-Free. We also investigate the Eventual Reception property for an extension of the type system. Some examples demonstrate the expressiveness of mixed choice in asynchronous multiparty protocols and the effectiveness of the proposed type discipline.

cs.LO↗

arXiv2026

Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday

Proof Theory and Type Theory are two branches of mathematical logic and theoretical computer science that explore the structure of mathematical proofs and the foundations of computation. Both are crucial for understanding formal systems, programming languages, and constructive mathematics. Stefano Berardi is an influential researcher in these fields, particularly known for his work on constructive logic, dependent types, and more recently, cyclic proofs. These proceedings intend to collect papers by researchers who are active in the field and often have been coauthors of Stefano, aimed to illustrate the achievements and the perspectives of this research area.

cs.LO↗

arXiv2025

Modular Multiparty Sessions with Mixed Choice

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 difficulty in controlling safety of communications. Such a control is more viable when modular systems are considered and the power of mixed choice fully exploited only inside loosely coupled modules. We carry over such idea in a type assignment approach to multiparty sessions. Typability for modular sessions entails Subject Reductions, Session Fidelity and Lock Freedom.

cs.LO↗

arXiv2024

Safe Composition of Systems of Communicating Finite State Machines

The Participants-as-Interfaces (PaI) approach to system composition suggests that participants of a system may be viewed as interfaces. Given a set of systems,one participant per system is chosen to play the role of an interface. When systems are composed, the interface participants are replaced by gateways which communicate to each other by forwarding messages. The PaI-approach for systems of asynchronous communicating finite state machines (CFSMs) has been exploited in the literature for binary composition only, with a (necessarily) unique forwarding policy. In this paper we consider the case of multiple system composition when forwarding gateways are not uniquely determined and their interactions depend on specific connection policies complying with a connection model. We represent connection policies as CFSM systems and prove that a bunch of relevant communication properties (deadlock-freeness, reception-error-freeness, etc.) are preserved by PaI multicomposition, with the proviso that also the used connection policy does enjoy the communication property taken into account.

cs.LO↗

arXiv2024

Partial Typing for Asynchronous Multiparty Sessions

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 system for multiparty sessions (i.e. sets of concurrent participants) with asynchronous communications. Sessions are possibly typed by "asynchronous global types" describing the overall behaviour of specific subsets of participants only (from which the word "partial"). Typability is proven to ensure that sessions enjoy the partial versions of the well-known properties of lock- and orphan-message-freedom.

cs.LO↗

arXiv2023

Partially Typed Multiparty Sessions

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 types representing interesting protocols, which have no type in the standard type systems. Our type system enjoys Subject Reduction, Session Fidelity and "partial" Lock-freedom. The last property ensures the absence of locks for participants with non ignored communications. A sound and complete type inference algorithm is also discussed.

cs.LO↗

arXiv2023

A Theory of Formal Choreographic Languages

We introduce a meta-model based on formal languages, dubbed formal choreographic languages, to study message-passing systems. Our framework allows us to generalise standard constructions from the literature and to compare them. In particular, we consider notions such as global view, local view, and projections from the former to the latter. The correctness of local views projected from global views is characterised in terms of a closure property. We consider a number of communication properties -- such as (dead)lock-freedom -- and give conditions on formal choreographic languages to guarantee them. Finally, we show how formal choreographic languages can capture existing formalisms; specifically we consider communicating finite-state machines, choreography automata, and multiparty session types. Notably, formal choreographic languages, differently from most approaches in the literature, can naturally model systems exhibiting non-regular behaviour.

cs.LO↗

arXiv2022

On Composing Communicating Systems

Communication is an essential element of modern software, yet programming and analysing communicating systems are difficult tasks. A reason for this difficulty is the lack of compositional mechanisms that preserve relevant communication properties. This problem has been recently addressed for the well-known model of communicating systems, that is sets of components consisting of finite-state machines capable of exchanging messages. The main idea of this approach is to take two systems, select a participant from each of them, and derive from those participants a pair of coupled gateways connecting the two systems. More precisely, a message directed to one of the gateways is forwarded to the gateway in the other system, which sends it to the other system. It has been shown that, under some suitable compatibility conditions between gateways, this composition mechanism preserves deadlock freedom for asynchronous as well as symmetric synchronous communications (where sender and receiver play the same part in determining which message to exchange). This paper considers the case of asymmetric synchronous communications where senders decide independently which message should be exchanged. We show here that preservation of lock freedom requires sequentiality of gateways, while this is not needed for preservation of either deadlock freedom or strong lock freedom.

cs.LO↗

arXiv2021

Composition of choreography automata

Choreography automata are an automata-based model of choreographies, that we show to be a compositional one. Choreography automata represent global views of choreographies (and rely on the well-known model of communicating finite-state machines to model local behaviours). The projections of well-formed global views are live as well as lock- and deadlock-free. In the class of choreography automata we define an internal operation of {\em composition}, which connects two global views via roles acting as interfaces. We show that under mild conditions the composition of well-formed choreography automata is well-formed. The composition operation enables for a flexible modular mechanism at the design level.

cs.FL↗

arXiv2019

Open Multiparty Sessions

Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described by means of global types. Typable multiparty session enjoy lock-freedom. We look at multiparty sessions as open systems by a suitable definition of connection transforming compatible processes into gateways (forwarders). A relation resembling the standard subtyping relation for session types is used to formalise compatibility. We show that the session obtained by connection can be typed by manipulating the global types of the starting sessions. This allows us to prove that lock-freedom is preserved by connection.

cs.LO↗

arXiv2018

Global Types for Open Systems

Global-type formalisms enable to describe the overall behaviour of distributed systems and at the same time to enforce safety properties for communications between system components. Our goal is that of amending a weakness of such formalisms: the difficulty in describing open systems, i.e. systems which can be connected and interact with other open systems. We parametrically extend, with the notion of interface role and interface connection, the syntax of global-type formalisms. Semantically, global types with interface roles denote open systems of communicating finite state machines connected by means of gateways obtained from compatible interfaces. We show that safety properties are preserved when open systems are connected that way.

cs.LO↗

arXiv2018

Intersection Types for the lambda-mu Calculus

We introduce an intersection type system for the lambda-mu calculus that is invariant under subject reduction and expansion. The system is obtained by describing Streicher and Reus's denotational model of continuations in the category of omega-algebraic lattices via Abramsky's domain-logic approach. This provides at the same time an interpretation of the type system and a proof of the completeness of the system with respect to the continuation models by means of a filter model construction. We then define a restriction of our system, such that a lambda-mu term is typeable if and only if it is strongly normalising. We also show that Parigot's typing of lambda-mu terms with classically valid propositional formulas can be translated into the restricted system, which then provides an alternative proof of strong normalisability for the typed lambda-mu calculus.

cs.LO↗

arXiv2017

Session Types for Orchestrated Interactions

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 operator of "speculative selection" including choices not necessarily offered by a compliant partner. We address the problem of selecting successful communicating branches by means of an operational semantics based on orchestrators, which has been shown to be equivalent to the retractable semantics of contracts, but clearly more feasible. A type system, sound with respect to such a semantics, is hence provided.

cs.LO↗

arXiv2017

Retractability, games and orchestrators for session contracts

Session contracts is a formalism enabling to investigate client/server interaction protocols and to interpret session types. We extend session contracts in order to represent outputs whose actual sending in an interaction depends on a third party or on a mutual agreement between the partners. Such contracts are hence adaptable, or as we say "affectible". In client/server systems, in general, compliance stands for the satisfaction of all client's requests by the server. We define an abstract notion of "affectible compliance" and show it to have a precise three-party game-theoretic interpretation. This in turn is shown to be equivalent to a compliance based on interactions that can undergo a sequence of failures and rollbacks, as well as to a compliance based on interactions which can be mediated by an orchestrator. Besides, there is a one-to-one effective correspondence between winning strategies and orchestrators. The relation of subcontract for affectible contracts is also investigated.

cs.LO↗

arXiv2016

Retractable Contracts

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 fails, the past agreements are good candidates as points where to roll back, in order to take a different agreement. We propose a variant of contracts with synchronous rollbacks to agreement points in case of deadlock. The new calculus is equipped with a compliance relation which is shown to be decidable.

cs.LO↗

arXiv2015

Orchestrated Session Compliance

We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. Devising the notion of orchestrator in such a context makes it possible to have orchestrators with unbounded buffering capabilities and at the same time to guarantee any message from the client to be eventually delivered by the orchestrator to the server, while preventing the server from sending messages which are kept indefinitely inside the orchestrator. The compliance relation is shown to be decidable by means of 1) a procedure synthesising the orchestrators, if any, making a client compliant with a server, and 2) a procedure for deciding whether an orchestrator behaves in a proper way as mentioned before.

cs.LO↗

arXiv2014

Loosening the notions of compliance and sub-behaviour in client/server systems

In the context of "session behaviors" for client/server systems, we propose a weakening of the compliance and sub-behaviour relations where the bias toward the client (whose "requests" must be satisfied) is pushed further with respect to the usual definitions, by admitting that "not needed" output actions from the server side can be "skipped" by the client. Both compliance and sub-behaviour relations resulting from this weakening remain decidable, though the proof of the duals-as-minima property for servers, on which the decidability of the sub-behaviour relation relies, requires a tighter analysis of client/server interactions.

cs.LO↗

arXiv2014

Compliance for reversible client/server interactions

In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via a LTS, and define a natural notion of checkpoint compliance. We then obtain a co-inductive characterisation of such compliance relation, and an axiomatic presentation that is proved to be sound and complete. As a byproduct we get a decision procedure for the new compliance, being the axiomatic system algorithmic.

cs.LO↗