arXiv subjects

Mariangiola Dezani-Ciancaglini

Publications and source records attributed to Mariangiola Dezani-Ciancaglini.

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

Sensible Intersection Type Theories

Finitary/static semantics in the form of intersection type assignments have become a paradigm for analysing the fine structure of all sorts of lambda-models. The key step is the construction of a filter model isomorphic to a given lambda-model. A property of great interest of filter lambda-models is sensibility, i.e. the interpretation of all unsolvable terms is the least element. The flexibility of intersection type assignments derives from their parametrisation on intersection type theories. We construe intersection type theories as special meet-semilattices and show that appropriate morphisms, in the opposite category of meet-semilattices, preserve sensibility of the induced lambda-models. Interestingly the set of saturated sets together with the set of lambda-terms is such a meet-semilattice, thus showing that arguments based on Tait-Girards's computability amount to the construction of a morphism. We characterise two classes of intersection type theories which induce sensible filter models. The first is non-effective while the second is effective and it amounts to the generalisation of Mendler's criterion to intersection types and head normalising terms. The complete characterisation of sensible filter models however still escapes.

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

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↗

arXiv2024

Global types and event structure semantics for asynchronous multiparty sessions

We propose an interpretation of multiparty sessions with asynchronous communication as Flow Event Structures. We introduce a new notion of global type for asynchronous multiparty sessions, ensuring the expected properties for sessions, including progress. Our global types, which reflect asynchrony more directly than standard global types and are more permissive, are themselves interpreted as Prime Event Structures. The main result is that the Event Structure interpretation of a session is equivalent, when the session is typable, to the Event Structure interpretation of its global type.

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

Deconfined Global Types for Asynchronous Sessions

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the accepted behaviours. Our type system improves the state-of-the-art by typing all asynchronous sessions and preserving the key properties of Subject Reduction, Session Fidelity and Progress when some well-formedness conditions are satisfied. The type system comes together with a sound and complete type inference algorithm. The well-formedness conditions are undecidable, but an algorithm checking an expressive restriction of them recovers the effectiveness of typing.

cs.LO↗

arXiv2022

Event structure semantics for multiparty sessions

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 multiparty sessions can be described by global types, to an interpretation of global types as "prime event structures".

cs.LO↗

arXiv2022

Asynchronous Sessions with Input Races

We propose a calculus for asynchronous multiparty sessions where input choices with different senders are allowed in processes. We present a type system that accepts such input races provided they do not hinder lock-freedom.

cs.LO↗

arXiv2020

Soundness conditions for big-step semantics

We propose a general proof technique to show that a predicate is sound, that is, prevents stuck computation, with respect to a big-step semantics. This result may look surprising, since in big-step semantics there is no difference between non-terminating and stuck computations, hence soundness cannot even be expressed. The key idea is to define constructions yielding an extended version of a given arbitrary big-step semantics, where the difference is made explicit. The extended semantics are exploited in the meta-theory, notably they are necessary to show that the proof technique works. However, they remain transparent when using the proof technique, since it consists in checking three conditions on the original rules only, as we illustrate by several examples.

cs.PL↗

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

Java & Lambda: a Featherweight Story

We present FJ&$λ$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, $λ$-expressions, and intersection types. Our main goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. We show how intersection types play a significant role in several cases, in particular in the typecast of a $λ$-expression and in the typing of conditional expressions. We also embody interface \emph{default methods} in FJ&$λ$, since they increase the dynamism of $λ$-expressions, by allowing these methods to be called on $λ$-expressions. The crucial point in Java 8 and in our calculus is that $λ$-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when $λ$-expressions come without target types. In particular, in the operational semantics we must record target types by decorating $λ$-expressions, otherwise they would be lost in the runtime expressions. We prove the subject reduction property and progress for the resulting calculus, and we give a type inference algorithm that returns the type of a given program if it is well typed. The design of FJ&$λ$ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&$λ$ programs are typed and behave the same as Java programs.

cs.LO↗

arXiv2017

On the Preciseness of Subtyping in Session Types

Subtyping in concurrency has been extensively studied since early 1990s as one of the most interesting issues in type theory. The correctness of subtyping relations has been usually provided as the soundness for type safety. The converse direction, the completeness, has been largely ignored in spite of its usefulness to define the largest subtyping relation ensuring type safety. This paper formalises preciseness (i.e. both soundness and completeness) of subtyping for mobile processes and studies it for the synchronous and the asynchronous session calculi. We first prove that the well-known session subtyping, the branching-selection subtyping, is sound and complete for the synchronous calculus. Next we show that in the asynchronous calculus, this subtyping is incomplete for type-safety: that is, there exist session types T and S such that T can safely be considered as a subtype of S, but T < S is not derivable by the subtyping. We then propose an asynchronous subtyping system which is sound and complete for the asynchronous calculus. The method gives a general guidance to design rigorous channel-based subtypings respecting desired safety properties. Both the synchronous and the asynchronous calculus are first considered with lin ear channels only, and then they are extended with session initialisations and c ommunications of expressions (including shared channels).

cs.LO↗

arXiv2017

On Sessions and Infinite Data

We define a novel calculus that combines a call-by-name functional core with session-based communication primitives. We develop a typing discipline that guarantees both normalisation of expressions and progress of processes and that uncovers an unexpected interplay between evaluation and communication.

cs.LO↗

arXiv2017

Retractions in Intersection Types

This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed.

cs.LO↗

arXiv2016

Reversible Multiparty Sessions with Checkpoints

Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or roll back to some checkpoints, where possibly different choices may be taken. In this way communications can be undone and different conversations may be tried. Interactions are typed with global types, which control also rollbacks. Typeability of session participants in agreement with global types ensures session fidelity and progress of reversible communications.

cs.LO↗

arXiv2016

Secure Multiparty Sessions with Topics

Multiparty session calculi have been recently equipped with security requirements, in order to guarantee properties such as access control and leak freedom. However, the proposed security requirements seem to be overly restrictive in some cases. In particular, a party is not allowed to communicate any kind of public information after receiving a secret information. This does not seem justified in case the two pieces of information are totally unrelated. The aim of the present paper is to overcome this restriction, by designing a type discipline for a simple multiparty session calculus, which classifies messages according to their topics and allows unrestricted sequencing of messages on independent topics.

cs.LO↗

arXiv2016

Parallel Monitors for Self-adaptive Sessions

The paper presents a data-driven model of self-adaptivity for multiparty sessions. System choreography is prescribed by a global type. Participants are incarnated by processes associated with monitors, which control their behaviour. Each participant can access and modify a set of global data, which are able to trigger adaptations in the presence of critical changes of values. The use of the parallel composition for building global types, monitors and processes enables a significant degree of flexibility: an adaptation step can dynamically reconfigure a set of participants only, without altering the remaining participants, even if the two groups communicate.

cs.LO↗