π-calculus, Session Types research at Imperial College

Tools & Software

Tools and software developed by our group.

Dynamic deadlock verification for general barrier synchronisation

Armus is a dynamic verification tool for deadlock detection and avoidance specialised in barrier synchronisation. Barriers are used to coordinate the execution of groups of tasks, and serve as a building block of parallel computing. Our tool verifies more barrier synchronisation patterns than current state-of-the-art. To improve the scalability of verification, we introduce a novel event-based representation of concurrency constraints, and a graph-based technique for deadlock analysis. The implementation is distributed and fault-tolerant, and can verify X10 and Java programs.

A domain-specific language for smart contracts with a computationally sound embedding into Bitcoin
DinGo hunter
Static deadlock detection tool for Go

dingo-hunter is a static deadlock detection tool for the Go language. The tool leverages session graph synthesis to detect potential deadlocks and unsafe concurrency patterns in the source code.

EMTST: Engineering the Meta-theory of Session Types
Libraries for mechanising the theory of session types calculi in Coq.
Effects as sessions, session as effects

The effect-sessions library is an implementation of session types in Haskell, via an effect system encoding by embedding session types into an effect system. (POPL’16 artifact)

Tool for synthesising a choreography from Genalised Multiparty Compatible CFSMs

The tool allows to

Godel Checker
Go model checker for MiGo types

godel-checker is a model checker for MiGo types, and uses the output of the MiGo type extractor gospal. This tool is part of the Go static verification framework described in this work.

Channel Liveness and Safety checker

Gong is a liveness and safety checker for MiGo types.

Happy Asynchronous Pi Calculus

HAPI is a programming language developed by Lasse Nielsen which provides an intuitive syntax for the asynchronous pi-calculus with multiparty session types.

a tool for checking k-multiparty compatibility in communicating session automata
Type-safe session programming in Scala

lchannels is a Scala library for type-safe session programming. It provides linear I/O channels, which allow to transfer data locally, or over a network. Its API allows to

  1. define protocols, represented as a set of continuation-passing style classes, and
  2. easily write programs that interact according to such protocols

The Scala type checker can examine the resulting code and spot many protocol violations at compile time.

Parameterised Scribble

Pabble is a parametric extension of Scribble primarily designed for describing communication protocols in parallel computing.

Parallel Algebraic Language
A Haskell EDSL for building session-typed parallel code.
Scribble Project
Protocol description language

The Scribble project is a joint effort with Cognizant, OOI and Red Hat established to realise multiparty session types as application-level protocols. It consists of a core language Scribble and tools/IDE support. A research version of Scribble is available from Raymond Hu, please contact him for details.


Scribble-Go is a toolchain for safe distributed programming using role-parametric session types in Go. It extends Scribble, a toolchain for safe distributed programming using basic (non-role-parametric) session types in Java, with:

A concurrent programming language with refined session types
SePi is a concurrent, message-passing programming language based on the pi-calculus. The language features synchronous, bi-directional channel-based communication. Programs use primitives to send and receive messages as well as offer and select choices. Channel interactions are statically verified against session types describing the kind and order of messages exchanged, as well as the number of processes that may share a channel. In order to facilitate a more precise control of program properties, SePi includes assume and assert primitives at the process level and refinements at the type level.
Session Actor
An actor framework in Python with support for session types

Session Actor is an actor framework in Python with support for session types. An actor can implement multiple session types (roles) in a similar way as an object can implement multiple interfaces. The framework supports automatic discovery of roles and runtime checks for protocol compliance.

Session C programming framework
Multiparty session programming in C

Session C is a communication-safe programming framework which combines multiparty session types with the C programming language.

Session Java
Session-based distributed programming in Java

A Java extension with support for Session Types.

Session OCaml
A novel library for concurrent/distributed programming in OCaml

Session-ocaml is an implementation of session types in OCaml.

Session Type Providers
STP is a type provider for F# that generates APIs from protocol specifications

STP is a type provider in F# that generates APIs from protocol specifications.

Let it recover: Multiparty Protocol Induced Recovery

This is an Erlang API for programming with gen_server.

We statically analyse the communication flow of a program, given as a multiparty protocol, to extract the causal dependencies between processes and to localise failures. A recovered communication system is free from deadlocks, orphan messages and reception errors.