This paper gives a complete characterisation of type isomorphism definable by terms of a λ-calculus with intersection and union types. Unfortunately, when union is considered the Subject Reduction property does not hold in general. However, it is well known that in the λ-calculus, independently of the considered type system, the isomorphism between two types can be realised only by invertible terms. Notably, all invertible terms are linear terms. In this paper, the isomorphism of intersection and union types is investigated using a relevant type system for linear terms enjoying the Subject Reduction property. To characterise type isomorphism, a similarity between types and a type reduction are introduced. Types have a unique normal form with respect to the reduction rules and two types are isomorphic if and only if their normal forms are similar.

A multiparty session forms a unit of structured communication among many participants which follow communication sequences specified as a global type. When a process is engaged in two or more sessions simultaneously, different sessions can be interleaved and can interfere at runtime. Previous work on multiparty session types has ignored session interleaving, providing a limited progress property ensured only within a single session, by assuming non-interference among different sessions and by forbidding delegation. This paper develops, besides a more traditional, compositionalcommunicationtype system, a novel staticinteractiontype system for global progress in dynamically interleaved and interfered multiparty sessions. The interaction type system infers causalities of channels making sure that processes do not get stuck at intermediate stages of sessions also in presence of delegation.

This paper aims at incorporating the notion of self-adaptiveness in the context of multiparty sessions, by focusing on the issue of ensuring correctness for dynamic adaptations. A formal framework is presented centred around these main ingredients: global types, monitors and global state. A global type represents the overall communication choreography. Its projections are the monitors, which set-up the protocols of the participants. The association of a monitor with a compliant process incarnates a single participant. It is the choreography that is updated at runtime, in response to changing conditions in the global state. Monitors result to be self-adaptive in the sense that they react to these changes by modifying themselves, in order to prescribe new behaviours to the participants.

The stochastic modelling of biological systems, coupled with Monte Carlo simulation of models, is an increasingly popular technique in bioinformatics. The simulation-analysis workflow may result computationally expensive reducing the interactivity required in the model tuning. In this work, we advocate the high-level software design as a vehicle for building efficient and portable parallel simulators for the cloud. In particular, the Calculus of Wrapped Components (CWC) simulator for systems biology, which is designed according to the FastFlow pattern-based approach, is presented and discussed. Thanks to the FastFlow framework, the CWC simulator is designed as a high-level workflow that can simulate CWC models, merge simulation results and statistically analyse them in a single parallel workflow in the cloud. To improve interactivity, successive phases are pipelined in such a way that the workflow begins to output a stream of analysis results immediately after simulation is started. Performance and effectiveness of the CWC simulator are validated on the Amazon Elastic Compute Cloud.

The stochastic simulation of biological systems is an increasingly popular technique in Bioinformatics. It is often an enlightening technique, especially for multi-stable systems which dynamics can be hardly captured with ordinary differential equations. To be effective, stochastic simulations should be supported by powerful statistical analysis tools. The simulation-analysis workflow may however result in being computationally expensive, thus compromising the interactivity required in model tuning. In this work we advocate the high-level design of simulators for stochastic systems as a vehicle for building efficient and portable parallel simulators. In particular, the Calculus of Wrapped Components (CWC) simulator, which is designed according to the FastFlow's pattern-based approach, is presented and discussed in this work. FastFlow has been extended to support also clusters of multi-cores with minimal coding effort, assessing the portability of the approach.

The stochastic simulation of biological systems is an increasingly popular technique in bioinformatics. It often is an enlightening technique, which may however result in being computational expensive. We discuss the main opportunities to speed it up on multi-core platforms, which pose new challenges for parallelisation techniques. These opportunities are developed in two general families of solutions involving both the single simulation and a bulk of independent simulations (either replicas of derived from parameter sweep). Proposed solutions are tested on the parallelisation of the CWC simulator (Calculus of Wrapped Compartments) that is carried out according to proposed solutions by way of the Fast Flow programming framework making possible fast development and efficient execution on multi-cores.

We present a new kind of ambient calculus in which the open capability is replaced by direct mobility of generic processes. The calculus comes equipped with a labelled transition system in which types play a major role: this system allows us to show interesting algebraic laws. As usual, types express the communication, access and mobility properties of the modelled system, and inferred types express the minimal constraints required for the system to be well behaved.

In [6, p. 317] Curry described a formal system assigning types to terms of the type-free λ -calculus. In [11] Scott gave a natural semantics for this type assignment and asked whether a completeness result holds. Inspired by [4] and [5] we extend the syntax and semantics of the Curry types in such a way that filters in the resulting type structure form a domain in the sense of Scott [12]. We will show that it is possible to turn the domain of types into a λ -model, among other reasons because all λ -terms possess a type. This model gives the completeness result for the extended system. By a conservativity result the completeness for Curry's system follows. Independently Hindley [8], [9] has proved both completeness results using term models. His method of proof is in some sense dual to ours. For λ -calculus notation see [1].