Software is increasingly organised centring on distributed communicating processes. This is especially true in large-scale distributed computing platforms such as the backend of popular Web-based services and public sector platforms for e-healthcare and e-science, which often provide lifelines of society. An application is organised as a dynamic collection of distributed components. The framework is based on interacting processes, which extends the traditional paradigm of functions and objects and which allows far more versatile and scalable organisation of software components. Assuring safety in such distributed systems is a vital societal concern: many platforms are long-lived, offer socially critical services, and collect security-sensitive data; safety violations, including security breaches, can have wide-ranging consequences, from temporary service outage to information leakage to exploitation of security vulnerability by criminal organisations. However, existing assurance methodologies are based on objects and functions: no well-established formal assurance methodologies are known for distributed systems. Large-scale distributed computing infrastructures are like skyscrapers used by hundreds of thousands of people, for building which the well-established structural engineering principles are used as a foundation of safe engineering. Can we establish the corresponding engineering principles for building software skyscrapers vital to modern society? Against this background, the central aim of this project is to establish a general, formally based safety assurance methodology for distributed systems, which we call conversation-based governance. The conversation-based governance starts from advanced types for capturing conversations, called multiparty session types (MPSTs), recently introduced by the PIs and extensively studied by researchers. Building on the latest theoretical results and on the PIs' ongoing collaborations with the project partners, we introduce the new development and assurance framework based on MPSTs. At the centre of our approach is a high-level, programming-language-agnostic MPST-based declarative protocol description language. The safety assurance in this framework is realised through verifications of distributed components against formal specifications in this protocol language, performed either statically (at the development time) or dynamically (at runtime), of which we place an emphasis on the latter: large-scale distributed systems are rarely amenable to static verification as a whole due to, for example, heterogeneous components, so that only the dynamic verification and enforcement can offer a comprehensive safety assurance. It is due to this emphasis on runtime policing of conversations that we call the proposed assurance framework, conversation-based governance. The project will establish this new methodology through the following tasks: (1) The development of a programing-language-agnostic protocol description language, called Scribble, and its open source tool chain, programming interfaces (APIs) and runtimes, backed up by a uniform type theory of MPSTs. (2) The development of an assertion language for specifying and verifying refined safety properties as elaboration of protocols, together with a policy language linked to the assertion language. Decentralised monitors backed up by a theory of the pi-calculus offer efficient, scalable runtime verification and enforcement. (3) Large-scale experiments through collaboration with project partners, realising formal safety assurance for real-world applications, including global cyberinfrastructure, enterprise software, and messaging middleware. Throughout the project, an extensive dialogue between theories and practice will be conducted, leading to truly effective principles and tools for general safety assurance methodologies of distributed systems vital for future IT infrastructures and society.

There is growing interest in distributed systems and architectures whose components are autonomous social parties such as humans and organisations. The parties in such systems interact with each other via their software agents for the purposes of exchanging information and services. The interactions normally take the form of conversations (as opposed to invocations) realised over asynchronous messaging. Naturally, a crucial area of study for computer science and software engineering is the specification and enactment of interaction protocols, that is, the rules of encounter by which parties in the system would interact. Considered as such, the notion of protocol represents a generalisation of the notion of "contract" advocated in Design by Contract approaches. A key question concerns the nature of contracts. Work in areas such as concurrency and Web services, has predominantly conceptualised protocols in terms of message ordering and occurrence constraints that must be respected by the parties' agents. We refer to such protocols as messaging protocols. Although messaging protocols serve the important purpose of distributed coordination, considered as contracts, they are too low-level for multiagent settings of autonomous parties. Specifically, they do not capture social constraints such as the commitments that are binding on the parties in the interaction. This gap represents a substantial opportunity. In real life, commitments in fact represent the atoms of what people normally understand as contracts. Commitments accommodate the balance between, on the one hand, autonomy and flexibility, and, on the other hand, correct behaviour. Commitment specifications capture stakeholder requirements in multiparty domains. Further, the states of commitments underlie most key performance indicators (KPIs) that stakeholders are interested in any multiagent domain. Work in commitment protocols in multiagent systems has made progress in developing computational abstractions for commitments. However, important challenges related to expressiveness and distributed enactment of commitment protocols have not even been adequately formulated, let alone tackled. Ensuring correct distributed enactment for expressive commitment protocols is crucial to realising the full value of commitments as a human-level architectural abstraction. The broad objective of Turtles is to bring commitment-based contracts to distributed computing. This project develops foundational theory, software, and methodology for building commitment-based distributed systems. To encourage wider adoption, the project will embed the algorithms in prototypes, and develop a tool-supported methodology for specifying and implementing social protocols. Further, Turtles will develop real systems based on use cases and practices from a number of industrial partners and evaluate these systems based on their feedback. The success of Turtles will enable capturing important subtleties of real-life social and business interactions and transform how we design software systems for crucial multiparty domains such as healthcare, disaster response, smart cities, banking, education, and e-commerce and e-business, where commitments are crucial.

There is growing interest in distributed systems and architectures whose components are autonomous social parties such as humans and organisations. The parties in such systems interact with each other via their software agents for the purposes of exchanging information and services. The interactions normally take the form of conversations (as opposed to invocations) realised over asynchronous messaging. Naturally, a crucial area of study for computer science and software engineering is the specification and enactment of interaction protocols, that is, the rules of encounter by which parties in the system would interact. Considered as such, the notion of protocol represents a generalisation of the notion of "contract" advocated in Design by Contract approaches. A key question concerns the nature of contracts. Work in areas such as concurrency and Web services, has predominantly conceptualised protocols in terms of message ordering and occurrence constraints that must be respected by the parties' agents. We refer to such protocols as messaging protocols. Although messaging protocols serve the important purpose of distributed coordination, considered as contracts, they are too low-level for multiagent settings of autonomous parties. Specifically, they do not capture social constraints such as the commitments that are binding on the parties in the interaction. This gap represents a substantial opportunity. In real life, commitments in fact represent the atoms of what people normally understand as contracts. Commitments accommodate the balance between, on the one hand, autonomy and flexibility, and, on the other hand, correct behaviour. Commitment specifications capture stakeholder requirements in multiparty domains. Further, the states of commitments underlie most key performance indicators (KPIs) that stakeholders are interested in any multiagent domain. Work in commitment protocols in multiagent systems has made progress in developing computational abstractions for commitments. However, important challenges related to expressiveness and distributed enactment of commitment protocols have not even been adequately formulated, let alone tackled. Ensuring correct distributed enactment for expressive commitment protocols is crucial to realising the full value of commitments as a human-level architectural abstraction. The broad objective of Turtles is to bring commitment-based contracts to distributed computing. This project develops foundational theory, software, and methodology for building commitment-based distributed systems. To encourage wider adoption, the project will embed the algorithms in prototypes, and develop a tool-supported methodology for specifying and implementing social protocols. Further, Turtles will develop real systems based on use cases and practices from a number of industrial partners and evaluate these systems based on their feedback. The success of Turtles will enable capturing important subtleties of real-life social and business interactions and transform how we design software systems for crucial multiparty domains such as healthcare, disaster response, smart cities, banking, education, and e-commerce and e-business, where commitments are crucial.

We aim to solve computing's most pressing problem - concurrency and distribution - by adapting one of computing's most successful concepts - the data type. Data types codify the structure of data; session types codify the structure of communication. Session types will enable a revolution in the development of concurrent and distributed software, making it cheaper to construct and maintain, and more reliable. Concurrency and distribution are computing's most pressing problem: unless we discover a way to routinely and reliably build concurrent and distributed systems, a half century of unprecedented technical progress will draw to a close. We are approaching the 50th anniversary of Moore's Law, the observation that component counts and clock speeds double every 18 months. No exponential improvement can continue forever, and recently this rule has changed: clock speeds now remain fixed while the number of processors doubles, so exploitation of concurrency is essential. Meanwhile, everyone now has a computer in their pocket, and these computers depend crucially on communication to achieve their function. We inhabit a world of web applications, cloud services, and mobile apps: society increasingly depends on a technological infrastructure of concurrent and distributed systems. Programming concurrent and distributed systems is notoriously difficult. Many solutions are based on shared memory, which requires the programmer to reason about every possible interleaving by which many processors access a common resource. Shared memory scales only to a certain point; it is not appropriate for programming the server farms that drive the web or for mobile applications. The most successful solutions so far appear to be those that replace shared memory with communication as the central structuring technique. Communication usually centres around the notion of a protocol, a series of operations in a specific order. However, direct support for protocols at the language level has been lacking, as compared with data types. The data type is one of computing's most successful concepts. Data types appear from the oldest programming language to the newest, and cover concepts ranging from a single byte to organised tables containing information on customers and orders. Types act as the fundamental unit of compositionality: the first thing a programmer writes or reads about each method is its data type, and type discipline guarantees that each call of a method matches its definition. Data types play a central role in all aspects of software, from architectural design to interactive development environments to efficient compilation. The analogue of the data type for concurrency and distribution is the session type. A session type codifies the notion of a protocol. Session types build on data types, as data types specify the lowest level of data exchange, upon which more complex protocols are built. Just as type discipline matches use and definition of a method, so session types ensure consistency between the two ends of a communication. We expect session types to play a role in all aspects of software. Today, architects discuss the high-level structure of a system in terms of its types, but must resort to informal notions of protocol to describe communication; in future, they will describe communication in terms of session types. Today, programmers use tools that let them search for methods and modules based on their type, and give immediate feedback if their program violates type discipline, but must resort to informal notions of protocol when coding communications; in future, they will search for components based on their session type, and get immediate feedback if their program violates session type discipline. Today, software tools exploit types to optimise code, but cannot exploit the informal notions of protocol to optimise communication; in future, communication middleware will exploit session types to support efficient messaging.

Communication is not only an essential organisation principle for emerging large-scale distributed applications, such as those for e-Commerce, e-Science, e-Healthcare and financial technology (FinTech): it is also an effective way to use computational resources, such as microservices and manycore chips. In this new paradigm, communication and concurrency are the norm in software development rather than a marginal concern, enabling architects and programmers to harness the power of hundreds or even thousands of concurrent processes interacting through *message passing*. However, for this paradigm there is no well-established methodology for software development with safety and security gurantee based on clear and mathematically accurate criteria on its behaviour. This leaves uncertainty on the correctness of the construction of distributed infrastructure. The aim of this fellowship is to establish general and practical foundations for safety enforcement of communication-intensive concurrent and distributed applications, building on a general theory of *multiparty session types*. Communications in a distributed application are commonly organised into multiple structured conversations (*protocols*) where a developer or programmer wishes to enforce *observabilities* of system behaviours to follow a safety and security criteria given by a protocol. Here *observability* of systems behaviours means a visible sequence of message exchanges with more complex information such as dependency of data, secure information, cost and timing of communications. In the multiparty session types, an end-point system properly carries out its responsibility, so that observable systems behaviours as a whole obey an agreed-upon protocol. Multiparty session types articulate the basic dynamics in a respective computing paradigm, thus serving as a foundation for modelling, specification, verification, systematic testing and certification, enhanced with other methods such as monitoring and logical assertions. This fellowship aims to fulfil this potential of multiparty session types as types for communication by carrying out experiments. To achieve this goal, the following technical objectives have been identified: 1. The establishment of a uniform type theory for multiparty session types capturing a full range of application-level protocols based on behavioural theory and game semantics, as a foundation of the whole methodology. 2. The establishment of a dependent and refinement type theory of specifications and verifications; and of a scalable algorithm to verify safety and security properties based on automata theory. 3. The development and release of an open-source toolchain, based on (1,2), combined with Application Programming Interface (API) and with industry tools. 4. A theoretically well-founded architecture which can efficiently monitor, trace, log and enforce correct observational behaviour against specifications written in (3). 5. Experiments through collaboration with academic and industry partners, realising formal safety and security assurance against advanced protocols for real-world applications, including multi robotics/UAVs, financial and healthcare systems. Throughout the research programme, an active and extensive dialogue between theories (1,2) and practice (3,4,5) will be the key enabler for reaching the goals of the fellowship, ultimately establishing cross-disciplinary and co-created ICT research. The project also links assurance methodologies based on session types to the standardisation for Cloud Computing (Cloud Native Computing Foundation) and to the public regulatory requirements for the documentation of financial and e-Healthcare protocols, meeting the goals of People at the Heart of ICT.