Search

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., Comment: In Proceedings DCM 2023, arXiv:2409.19298

In this paper, we explore the concept of Mutually Unbiased Bases (MUBs) in discrete quantum systems. It is known that for dimensions $d$ that are powers of prime numbers, there exists a set of up to $d+1$ bases that form an MUB set. However, the maximum number of MUBs in dimensions that are not powers of prime numbers is not known. To address this issue, we introduce three algorithms based on First-Order Logic that can determine the maximum number of bases in an MUB set without numerical approximation. Our algorithms can prove this result in finite time, although the required time is impractical. Additionally, we present a heuristic approach to solve the semi-decision problem of determining if there are $k$ MUBs in a given dimension $d$. As a byproduct of our research, we demonstrate that the maximum number of MUBs in any dimension can be achieved with definable complex parameters, computable complex parameters, and other similar fields., Comment: 11 pages, 0 figures

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., Comment: In Proceedings ICE 2023, arXiv:2308.08920

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., Comment: In Proceedings PLACES 2022, arXiv:2203.12142

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"., Comment: arXiv admin note: text overlap with arXiv:2102.00865

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.

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.

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.

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., Comment: In Proceedings ICE 2019, arXiv:1909.05242

We present FJ&$\lambda$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, $\lambda$-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 $\lambda$-expression and in the typing of conditional expressions. We also embody interface \emph{default methods} in FJ&$\lambda$, since they increase the dynamism of $\lambda$-expressions, by allowing these methods to be called on $\lambda$-expressions. The crucial point in Java 8 and in our calculus is that $\lambda$-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when $\lambda$-expressions come without target types. In particular, in the operational semantics we must record target types by decorating $\lambda$-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&$\lambda$ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&$\lambda$ programs are typed and behave the same as Java programs.

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., Comment: In Proceedings ITRS 2016, arXiv:1702.01874

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., Comment: 39 pages 6 files including .bbl

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).

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., Comment: In Proceedings EXPRESS/SOS 2016, arXiv:1608.02692

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., Comment: In Proceedings PLACES 2016, arXiv:1606.05403

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., Comment: In Proceedings PLACES 2016, arXiv:1606.05403

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., Comment: In Proceedings PLACES 2015, arXiv:1602.03254

The notion of subtyping has gained an important role both in theoretical and applicative domains: in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different points of view: operational and denotational. The former preciseness has been recently developed with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. The latter preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The result of this paper is the operational and denotational preciseness of the subtyping for a synchronous multiparty session calculus. The novelty of this paper is the introduction of characteristic global types to prove the operational completeness., Comment: In Proceedings PLACES 2015, arXiv:1602.03254

Today's software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.

Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the right type. The present paper faces the problem of type isomorphism in a system with intersection and union types. In the presence of intersection and union, isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, quite complicated by the interference between functional and non functional types. This drawback is faced in the paper by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This choice has been suggested by the initial projection of Scott's inverse limit lambda-model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction., Comment: In Proceedings ITRS 2014, arXiv:1503.04377

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., Comment: In Proceedings BEAT 2014, arXiv:1408.5564

We present initial results on a comprehensive model of structured communications, in which self- adaptation and security concerns are jointly addressed. More specifically, we propose a model of self-adaptive, multiparty communications with secure information flow guarantees. In this model, security violations occur when processes attempt to read or write messages of inappropriate security levels within directed exchanges. Such violations trigger adaptation mechanisms that prevent the violations to occur and/or to propagate their effect in the choreography. Our model is equipped with local and global mechanisms for reacting to security violations; type soundness results ensure that global protocols are still correctly executed, while the system adapts itself to preserve security., Comment: In Proceedings BEAT 2014, arXiv:1408.5564

There has been a considerable amount of work on retrieving functions in function libraries using their type as search key. The availability of rich component specifications, in the form of behavioral types, enables similar queries where one can search a component library using the behavioral type of a component as the search key. Just like for function libraries, however, component libraries will contain components whose type differs from the searched one in the order of messages or in the position of the branching points. Thus, it makes sense to also look for those components whose type is different from, but isomorphic to, the searched one. In this article we give semantic and axiomatic characterizations of isomorphic session types. The theory of session type isomorphisms turns out to be subtle. In part this is due to the fact that it relies on a non-standard notion of equivalence between processes. In addition, we do not know whether the axiomatization is complete. It is known that the isomorphisms for arrow, product and sum types are not finitely axiomatisable, but it is not clear yet whether this negative results holds also for the family of types we consider in this work., Comment: In Proceedings PLACES 2014, arXiv:1406.3313

This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types., Comment: In Proceedings ITRS 2012, arXiv:1307.7849

BioScape is a concurrent language motivated by the biological landscapes found at the interface of biology and biomaterials. It has been motivated by the need to model antibacterial surfaces, biofilm formation, and the effect of DNAse in treating and preventing biofilm infections. As its predecessor, SPiM, BioScape has a sequential semantics based on Gillespie's algorithm, and its implementation does not scale beyond 1000 agents. However, in order to model larger and more realistic systems, a semantics that may take advantage of the new multi-core and GPU architectures is needed. This motivates the introduction of parallel semantics, which is the contribution of this paper: Parallel BioScape, an extension with fully parallel semantics., Comment: In Proceedings MeCBIC 2012, arXiv:1211.3476

In this paper we present a variant of the Calculus of Looping Sequences (CLS for short) with global and local rewrite rules. While global rules, as in CLS, are applied anywhere in a given term, local rules can only be applied in the compartment on which they are defined. Local rules are dynamic: they can be added, moved and erased. We enrich the new calculus with a parallel semantics where a reduction step is lead by any number of global and local rules that could be performed in parallel. A type system is developed to enforce the property that a compartment must contain only local rules with specific features. As a running example we model some interactions happening in a cell starting from its nucleus and moving towards its mitochondria., Comment: In Proceedings DCM 2011, arXiv:1207.6821

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 restrictions are semantically justified. The multi-party sessions obtained projecting our global types enjoy a liveness property in addition to the traditional progress and are shown to be sound and complete with respect to the set of traces of the originating global type. Our notion of completeness is less demanding than the classical ones, allowing a multi-party session to leave out redundant traces from an underspecified global type. In addition to the technical content, we discuss some limitations of our language of global types and provide an extensive comparison with related specification languages adopted in different communities.

We consider a calculus for multiparty sessions enriched with security levels for messages. We propose a monitored semantics for this calculus, which blocks the execution of processes as soon as they attempt to leak information. We illustrate the use of our monitored semantics with various examples, and show that the induced safety property implies a noninterference property studied previously., Comment: In Proceedings EXPRESS 2011, arXiv:1108.4077

We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term with free variables, representing open code, can be packed into an "unbound" term, and passed around as a value. In order to execute inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type decorated with k if it needs k rebinds in order to reduce to a value. With intersection types we model the fact that a term can be used differently in contexts providing different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a value type, that is, an intersection type where at least one element has level 0. With the proposed intersection type system we get soundness under the call-by-value strategy, an issue which was not resolved by previous type systems., Comment: In Proceedings ITRS 2010, arXiv:1101.4104

In this work we study the convex set of quantum states from a quantum logical point of view. We consider an algebraic structure based on the convex subsets of this set. The relationship of this algebraic structure with the lattice of propositions of quantum logic is shown. This new structure is suitable for the study of compound systems and shows new differences between quantum and classical mechanics. This differences are linked to the nontrivial correlations which appear when quantum systems interact. They are reflected in the new propositional structure, and do not have a classical analogue. This approach is also suitable for an algebraic characterization of entanglement.

The Stochastic Calculus of Looping Sequences is suitable to describe the evolution of microbiological systems, taking into account the speed of the described activities. We propose a type system for this calculus that models how the presence of positive and negative catalysers can modify these speeds. We claim that types are the right abstraction in order to represent the interaction between elements without specifying exactly the element positions. Our claim is supported through an example modelling the lactose operon.

The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. We enrich this calculus with a type discipline to guarantee the soundness of reduction rules with respect to some biological properties deriving from the requirement of certain elements, and the repellency of others. As an example, we model a toy system where the repellency of a certain element is captured by our type system and forbids another element to exit a compartment.