17 citations · 90 across the 19 of their papers we have counts for
19 papers
Safe Composition of CFSM Systems via Partial Gateways
Franco Barbanera
The Participants-as-Interfaces (PaI) methodology for system composition proposes that system participants can be regarded as interfaces. For each system in a given collection, one…
Asynchronous Multiparty Sessions with Mixed Choice
Franco Barbanera, Mariangiola Dezani-Ciancaglini
We present an asynchronous calculus for multiparty sessions with mixed choice, which extends the Simple MultiParty Session framework in order to support nondeterministic choices wi…
Logics and Type Theory: essays dedicated to Stefano Berardi on the occasion of his 1000000th birthday
Thorsten Altenkirch, Franco Barbanera, Ferruccio Damiani +1
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 comput…
Modular Multiparty Sessions with Mixed Choice
Franco Barbanera, Mariangiola Dezani-Ciancaglini
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 receiv…
Partial Typing for Asynchronous Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de'Liguoro
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…
Partially Typed Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini
A multiparty session formalises a set of concurrent communicating participants. We propose a type system for multiparty sessions where some communications between participants can…
A Theory of Formal Choreographic Languages
Franco Barbanera, Ivan Lanese, Emilio Tuosto
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 constru…
On Composing Communicating Systems
Franco Barbanera, Ivan Lanese, Emilio Tuosto
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 compo…
Composition of choreography automata
Franco Barbanera, Ivan Lanese, Emilio Tuosto
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 rel…
Open Multiparty Sessions
Franco Barbanera, Mariangiola Dezani-Ciancaglini
Multiparty sessions are systems of concurrent processes, which allow several participants to communicate by sending and receiving messages. Their overall behaviour can be described…
Global Types for Open Systems
Franco Barbanera, Ugo de'Liguoro, Rolf Hennicker
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 component…
Session Types for Orchestrated Interactions
Franco Barbanera, Ugo de'Liguoro
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 the…
Intersection Types for the lambda-mu Calculus
Steffen van Bakel, Franco Barbanera, Ugo de'Liguoro
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…
Retractability, games and orchestrators for session contracts
Franco Barbanera, Ugo de'Liguoro
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 outpu…
Retractable Contracts
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ivan Lanese +1
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 agre…
Orchestrated Session Compliance
Franco Barbanera, Steffen van Bakel, Ugo de'Liguoro
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…
Compliance for reversible client/server interactions
Franco Barbanera, Mariangiola Dezani-Ciancaglini, Ugo de' Liguoro
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…
Loosening the notions of compliance and sub-behaviour in client/server systems
Franco Barbanera, Ugo de' Liguoro
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 "reque…
Characterisation of Strongly Normalising lambda-mu-Terms
Steffen van Bakel, Franco Barbanera, Ugo de'Liguoro
We provide a characterisation of strongly normalising terms of the lambda-mu-calculus by means of a type system that uses intersection and product types. The presence of the latter…