We present our preliminary work towards a comprehensive solution for the hybrid (static + dynamic) verification of open distributed systems, using session types. We automate a solution for binary sessions where one
Concrete artefacts are produced and used for dissemination. These include scientific publications, a repository of use-cases, tutorials, a non-technical article presenting the main achievements of the project, material for tutorials and recorded tutorials. These artefacts will remain available to the general public beyond the duration of the project and promote a continuative and long-term dissemination.
There are two approaches to defining subtyping relations: the syntactic and the semantic approach. In semantic subtyping, one defines a model of the language and an interpretation of types as
This is a tutorial paper on [St]Mungo, a toolchain based on multiparty session types and their connection to typestates for safe distributed programming in Java language. The StMungo (Scribble-to-Mungo) tool
We discuss the relationship between session types and behavioural contracts under the assumption that processes communicate asynchronously. We show the existence of a fully abstract interpretation of session types into
Following previous work on the automated deployment of componentbased applications, we present a formal model specifically tailored for reasoning on the deployment of microservice architectures. The first result that we
In Choreographic Programming, a choreography specifies in a single artefact the expected behaviour of all the participants in a distributed system. The choreography is used to synthesise correct-by-construction programs for
Automata models are well-established in many areas of computer science and are supported by a wealth of theoretical results including a wide range of algorithms and techniques to specify and