Self-adaptation and secure information flow in multiparty communications

We present a comprehensive model of structured communications in which self-adaptation and security concerns are jointly addressed. More specifically, we propose a model of multiparty, self-adaptive communications with access control and secure information flow guarantees. In our model, multiparty protocols (choreographies) are described as global types; security violations occur when process implementations of protocol participants 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 adaptation mechanisms for reacting to security violations of different gravity; type soundness results ensure that the overall multiparty protocol is still correctly executed while the system adapts itself to preserve the participants’ security.     

From Böhm's Theorem to Observational Equivalences: an Informal Account

There are essentially two ways of looking at the computational behaviours of λ-terms. One consists in putting the term within a context (possibly of λ-calculus extensions) and observing some properties (typically termination). The other consists in reducing the term until some meaningful information is obtained: this naturally leads to a tree representation of the information implicitly contained in the original term. The paper is an informal overview of the role played by Böhm's Theorem in these observations of terms.     

Can Addresses be Types?: A case study: objects with delegation

We adapt the aliasing constraints approach for designing a flexible typing of evolving objects. Types are singleton types (addresses of objects, as a matter of fact) whose relevance is mainly due to the sort of safety property they guarantee. In particular we provide a type system for an imperative object based calculus with delegation and which supports method and delegate overriding, addition, and removal.     

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 and of output skipping is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via an LTS, and define natural notions of checkpoint compliance and sub-behaviour, which we prove to be both decidable. Then we extend the operational semantics with skips and we show the decidability of the obtained compliance.     

Type Directed Semantics for the Calculus of Looping Sequences

The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. Here we enrich this calculus with a type discipline which preserves some biological properties deriving from the requirement of certain elements, and the repellency of others. In particular, the type system guarantees the soundness of the application of reduction rules with respect to the elements which are required (all requirements must be satisfied) and to the elements which are excluded (two elements which repel each other cannot occur in the same compartment). As an example, we model the possible interactions (and compatibility) of di?erent blood types with different antigens. The type system does not allow transfusion with incompatible blood types.     

Discrimination by Parallel Observers: The Algorithm

The main result of the paper is a constructive proof of the following equivalence: two pureλ-terms are observationally equivalent in the lazy concurrentλ-calculusiffthey have the same Lévy–Longo trees. An algorithm which allows to build a context discriminating any two pureλ-terms with different Lévy–Longo trees is described. It follows that contextual equivalence coincides with behavioural equivalence (bisimulation) as considered by Sangiorgi. Another consequence is that the discriminating power of concurrent lambda contexts is the same as that of Boudol–Laneve's contexts with multiplicities.     

Reduction of storage employed to represent families of information structures

The aim of this paper is to analyze a representation of information structures which minimizes the storage employed for their memorization. These structures must belong to a family satisfying given conditions. This representation is realized by constructing alisting, which is a one-one correspondence between the family of information structures and the setD of non-negative integers. The listing algorithm presented in this paper is an extension of that one given in [5]. The run time of both these listing algorithms and the resulting saving of storage are analyzed. As examples of application of the extended listing method, the listings of the family of structured programs according to [1] and of the families of ordered and non-ordered forest structures are treated extensively.

---

Sommario Lo scopo di questo lavoro è studiare un metodo di rappresentazione di strutture informative, che soddisfano condizioni date, tale da minimizzare lo spazio necessario per la loro memorizzazione. Tale metodo di rappresentazione è realizzato mediante la costruzione di una corrispondenza biunivoca tra la famiglia di strutture informative e l'insiemeD dei numeri interi non negativi. L'algoritmo che realizza tale corrispondenza qui presentato è una estensione dell'algoritmo dato in [5]; di entrambi gli algoritmi è data una analisi sia del tempo di esecuzione sia dello spazio di memoria occupato. Infine, a totolo di esempio, il metodo qui presentato è applicato alla famiglia dei programmi strutturati secondo [1] e alle famiglie delle strutture a foresta ordinata e non ordinata.

     

Filter models for conjunctive-disjunctive λ-calculi

The distinction between the conjunctive nature of non-determinism as opposed to the disjunctive character of parallelism constitutes the motivation and the starting point of the present work. λ-calculus is extended with both a non-deterministic choice and a parallel operator; a notion of reduction is introduced, extending β-reduction of the classical calculus. We study type assignment systems for this calculus, together with a denotational semantics which is initially defined constructing a set semimodel via simple types. We enrich the type system with intersection and union types, dually reflecting the disjunctive and conjunctive behaviour of the operators, and we build a filter model. The theory of this model is compared both with a Morris-style operational semantics and with a semantics based on a notion of capabilities.