Skip to end of metadata
Go to start of metadata
This page describes and references the theory about session types and its application in form of conversations


A fundamental challenge in modern computing is the establishment of effective and widely applicable development methodologies for distributed applications, comparable in their usability to the traditional methodologies for non-distributed software built on, among others, core UML diagrams and object-oriented programming languages. Although a middle-to-large-scale application is almost always distributed nowadays, and in spite of the presence of an accelerating infrastructural support for portable and reliable distributed components through e.g. clouds, software developers (including architects, designers and programmers alike) are still lacking well-established development methodologies for building systems centering on distributed processes and their interactions. For example, there is no central computational abstractions (comparable to classes and objects) for capturing distributed interactions usable throughout development stages; no UML diagrams are widely in use for modeling distributed applications; no major programming languages offer high-level, type-safe communication primitives, leaving treatment of communications to low-level APIs. In short, we are yet to have a general and tangible framework for developing distributed, communication-centered software systems.

We believe that one of the major reasons why it is so hard to even conceive an effective software development framework for distributed systems, is the lack of a core descriptive framework, with a uniform conceptual and formal foundation and usable throughout development stages. To illustrate this point, let us briefly examine the descriptive framework in one of the traditional development methodologies for non-distributed software, underpinned by UML diagrams and object-oriented programming. In this framework, the description of computation centres on objects (which belong to classes) and operations on objects, a representative paradigm of sequential computation. Class Diagram in UML and all associated core modelling diagrams such as Sequence Diagrams and State Charts follow this paradigm; and it is supported by many high-level programming languages, including Java, C++, C♯ and Python.

In the light of this well-established (and highly successful) engineering framework in the traditional development methodology, a natural question is whether we can build its analogue in the world of distributed processes, centred on common high-level abstraction for modelling and programming, and aiding modular software development on a rigorous theoretical basis.

Our main idea is that a distributed system can be naturally and effectively articulated as a collection of possibly overlapping structured conversations, and that the structures of these conversations, or protocols, can be clearly and accurately described using a type theory of the π-calculus, called session types.


Protocols in Interactional Computing.

The idea of protocols becomes important for general software development when the shape of software becomes predominantly a collection of numerous distributed processes communicating with each other. Such interactional computing is increasingly common in practice, from web services to financial protocols to services in clouds to parallel algorithms to multicore chips. Processes will be engaged in many interleaving conversations, each obeying a distinct protocol: the aggregate of overlapping conversations make up a whole distributed system. Dividing the design into distinct conversations promote tractability because the structure of one conversation in an application are relatively unaffected by other conversations. A protocol offers an agreement on the ways interactions proceed among two or more participants. Without such an agreement, it is hard to do meaningful interactions: participants cannot communicate effectively, since they do not know when the other parties will send what kind of data and through which channels. This is why the need to describe protocols have been observed in many different
contexts in the practice of interactional computing, as we illustrate below.


The Ocean Observatories Initiative (OOI) is a large-scale project funded by US National Science Foundation for implementation of a distributed environmental science observatory with persistent and interactive capabilities that have a global physical observatory footprint [17,42]. A key component of the OOI is a comprehensive cyberinfrastructure (CI), whose design is based on loosely coupled distributed services and agents, expected to reside throughout the OOI observatories, from seafloor instruments to on-shore research stations. The CI acts as an integrating element that links the sub-networks of OOI into a coherent system-of-systems and uses a large catalogue of communication protocols among distributed instruments and stakeholders. These protocols are required to be unambiguously specified for the implementation and runtime communication monitoring.

Conversation theory

Session types

As a type foundation for structured distributed, communication-centered programming, session types have been studied over the last decade for a wide range of process calculi and programming languages. The original binary theory has been generalized to multiparty session types in order to guarantee stronger conformance to stipulated session structures between cooperating multiple end-point participants. Since the first work was proposed, a multiparty session type theory has been developed in process calculi, and used in several different contexts such as distributed object communication optimisations, security, design by contract, parallel and web service programming and medical guidelines.


Scribble is a language to describe application-level protocols among communicating systems. A protocol represents an agreement on how participating systems interact with each other. Without a protocol, it is hard to do a meaningful interaction: participants simply cannot communicate effectively, since they do not know when to expect the other parties to send their data, or whether the other party is ready to receive a datum it is sending. In fact it is not clear what kinds of data is to be used for each interaction. It is too costly to carry out communications based on guess works and with inevitable communication mismatch (synchronisation bugs). Simply, it is not feasible as an engineering practice.

Scribble presents a stratified description language:

  • The bottom layer is the type layer, in which we describe the bare skeleton of conversations structures as types for interactions (known in the literature as session type).
  • The assertion layer allows elaboration of a type-layer description using assertions.
  • Finally the third layer, protocol document layer, allows description of multiple protocols and constraints over them.

Each layer offers distinct behavioural assurance for validated programs.
The development and validation of programs against protocol descriptions could proceed as follows:

  • A programmer specifies a set of protocols to be used in her application.
  • She can verify that those protocols are valid, free from livelocks and deadlocks.
  • She develops her application referring to those protocols, potentially using communication constructs available in the chosen programming language.
  • She validates her programs against protocols using a protocol checker, which detects lack of conformance.
  • At the execution time, a local monitor can validate messages with respect to given protocols, optionally blocking invalid messages from being delivered.


Multiparty Session Types (POPL'08)


Use of Scribble in ION

Scribble is the specification language for conversation protocols between distributed processes.

Prototyping occurs in Release 2 with application in construction to monitor RPC-based conversations between services.

See here for detailed documentation of Scribble:

Enter labels to add to this page:
Please wait 
Looking for a label? Just start typing.