Nowadays distributed computing systems are based on a simple paradigm of asynchronous message passing, since communication is the key feature of such systems and message passing is a natural way of modelling interaction. However, a global computing scenario poses new problems that are not present in the classical sequential and centralised systems. Situations like (partial) failures, disruption of connections, code mobility, dynamic reconfiguration of networks, make this domain intrinsically complex, whose analysis is particularly challenging. Moreover, the demand for safe and trustworthy applications and systems is increasing, as users become aware of the vulnerability of their present systems.

Solid mathematical foundations are essential to provide such guarantees. Provably correct solutions require rigorous mathematical models and analysis techniques, so that one may define precisely what are the problems to address, and how to perform proofs for the claimed properties. To express and prove properties logical systems are needed, but since most interesting properties are undecidable one cannot find complete proof systems. Furthermore, some decidable properties are intrinsically difficult to verify.

The typical solution is to use a decidable static analysis system (correct by over-approximating, but necessarily incomplete), of low computational complexity (to be of practical to use). A popular approach is the use of type systems to discipline the computational mechanisms programming languages, disallowing interactions that may lead to erroneous operations. Types are abstract representations of the correct behaviour of the entities of a program. A language is type safe, if it is equipped with a type (proof) system that guarantees that if a program is typable, the computation mechanism preserves the typability of the intermediate steps, and the absence of run-time errors.

The goal of the project is to develop new type systems to statically verify behavioural and structural properties of global, distributed open systems. We shall pursue our previous work on three inter-related subjects: non-uniform types for concurrent objects, investigating decidability issues; session types for component interoperability, investigating their extension to multi-party protocols; spatial types, investigating static analyses methods to prove not only behavioural and but also structural properties of distributed systems. Moreover, we plan to study the relationship between behavioural and session types, looking for a unified notion and system, and to relate spatial to behavioural types, characterising the latter in terms of the former.