MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Talks & Presentations

Recent invited talks and presentations from our group.

Mandrake: Building Fault-Tolerant Decentralized Applications
MRG meeting, Imperial College London

A decentralized application is constituted from independently-constructed software agents that represent autonomous principals. An outstanding challenge in distributed systems is how to coordinate the agents so that they can realize application meaning (the computations envisaged by the users of the application) but without relying on ordering mechanisms fixed in the application’s infrastructure. Forget causal delivery, even TCP is out! He will introduce Mandrake, a programming model for decentralized applications that tackles this challenge. Specifically, He will introduce the idea of specifying an application as an information protocol and then show how to construct protocol-compliant agents that communicate via UDP and can deal with transient failures that manifest as message loss. He will discuss Mandrake in the context of important systems ideas such as the end-to-end argument and why it achieves some of the goals of the founders of networked computing.

Date 6 May 2021
Speakers
Deconfined Global Types for Asynchronous Sessions
MRG meeting, Imperial College London

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the behaviours accepted. The global types presented in this paper improve the state-of-the-art by extending the set of typeable asynchronous sessions and preserving decidability of type checking together with the key properties of Subject Reduction, Session Fidelity and Progress

Date 22 Apr 2021
Speakers
Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
CC 2021

Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.

We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.

RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.

We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.

Date 3 Mar 2021
Speakers
Choreography Automata
MRG meeting, Imperial College London

Automata models are well-established in many areas of com-puter science and are supported by a wealth of theoretical results including a wide range of algorithms and techniques to specify and analyse systems. We introduce choreography automatafor the choreographic modelling of communicating systems. The projection of a choreography automaton yields a system of communicating finite-state machines. We consider both the standard asynchronous semantics of communicating systems and a synchronous variant of it. For both, the projections of well-formed automata are proved to be live as well as lock- and deadlock-free.

Date 16 Feb 2021
Speakers
Generating Deadlock-Free and Live Go Code From Unbounded Multiparty Session Protocols
Project meeting with Barclays

Go is a statically-typed language for building software in production environments. Its main goal is to provide a reliable and efficient way for developers to write communicating programs. Unfortunately recent work reveals that there are (surprisingly) many concurrent bugs in Go programs, more than half of which are caused by message-passing. A promising approach is the use of session types, a typing discipline that guarantees the absence of deadlocks and communication errors. Yet previous session type-based frameworks do not support dynamic unbounded participants, and cannot express many common Go programming patterns.

In this talk, I present GoScr (Go-Scribble), a toolchain for generating callback-style Go implementations from protocol specifications with unbounded, dynamic participants. GoScr guarantees, by construction, that the different participants will only perform I/O actions that comply with a given protocol specification, and that protocols are deadlock-free and live. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a noughts and crosses game with Min-Max strategy) in GoScr that could not be represented with previous theories of session types.

Date 15 Feb 2021
Speakers
Intersection Types and Runtime Errors in the Pi-Calculus
MRG meeting, Imperial College London

In this talk, I will survey our POPL 2019 paper introducing a type system for the π-calculus which guarantees that typable processes are well-behaved, in the sense that they never produce a run-time error and, even if they may diverge, there is always achance for them to “finish their work”, i.e., to reduce to an idle process. The type system is based on non-idempotent intersections, and is thus very powerful as for the class of processes it can capture. Indeed, despite the fact that the underlying property is Pi^0_2-complete, there is a way of showing that the system is complete, i.e., that any well-behaved process is typable, although for obvious reasons infinitely many derivations need to be considered.

Date 3 Nov 2020
Speakers
Session Subtyping and Multiparty Compatibility using Circular Sequents
MRG meeting, Imperial College London
Date 22 Oct 2020
Speakers
Global Types with Internal Delegation and Connecting Communications
MRG meeting, Imperial College London
Date 9 Oct 2020
Speakers
Effect handler oriented programming
MRG meeting, Imperial College London

Real world effects are pervasive, e.g.: concurrency, distribution, exceptions, I/O, and nondeterminism. Effect handlers are a general programming feature that can be used for modularly implementing all of these effects and more. They were introduced by theoretical computer scientists studying the theory of algebraic effects, but now show promise as a practical programming tool. Interest in effect handlers in industry is growing. For instance, Facebook’s React Fiber, the core of the popular React UI library is directly inspired by effect handlers, and Uber’s Pyro tool for probabilistic programming and GitHub’s Semantic library for parsing, analysing, and comparing source code (currently used for code navigation on over 4.5 million public Python repositories) both make essential use of effect handlers.

I will give an overview of effect handler oriented programming by way of a collection of examples and an operational semantics. In particular I will focus on concurrency examples. I will also briefly outline some of my contributions to the theory and practice of effect handler oriented programming as well as discussing challenges and future opportunities.

Date 18 Feb 2020
Speakers
Behavioural Type-based Static Verification Framework for Go
Kyoto University (30/07), Tohoku University (01/08), Waseda University (09/09)

I first give an overview of recent researches of my group.

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

Date 30 Jul 2019 - 9 Sep 2019
Speakers
Fluid Types: Statically Verified Distributed Protocols with Refinements
Facebook London (Type My Morning Seminar)

We present an end-to-end solution for verified distributed programming. Building upon the foundation of Multiparty Session Types with refinements, we propose a programming language with refinement types and discuss an API generation strategy to allow type checking to statically validate the refinements from the specification of the protocol to the implementation of each of its clients.

Date 17 May 2019
Speakers
The Security of Bitcoin
MRG meeting, Imperial College London

According to the folklore, Bitcoin would resist attacks unless the adversaries control the majority of the total computing power of the Bitcoin network. Unfortunately, many scientific works showed that reality is different. This presentation will address Bitcoin security from a theoretical and practical perspective. Firstly, by diving into the details of the protocol, we will prove some fundamental proprieties and the adversarial bound required for its security. Next, we will see some attacks that can exploit Bitcoin weaknesses.

Date 20 Feb 2019
Speakers
Behavioural Type-Based Static Verification Framework for Go
EUTYPES 2018, Aarhus University, Denmark

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work, we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioral types, where the types are model checked for liveness and safety.

Date 8 Oct 2018
Speakers
Distributed Programming using Role-Parametric Multiparty Session Types in Go
Guest seminar, Western Norway University of Applied Sciences, Norway

In this talk I will present a programming framework for static specification and safe programming of message passing protocols where the number and kinds of participants are dynamically instantiated. Our framework is based on Multiparty Session Types (MPST), extended to support parameterised protocols with indexed roles - where the number of roles is known only at run time.

Our framework statically infers the different kinds of participants induced by a protocol definition as role variants, and produces decoupled endpoint projections of the protocol onto each participant. This enables communication-safe, deadlock-free programming of the parameterised endpoint in distributed settings: each endpoint can be implemented (and verified) separately by different programmers/technique/languages.

We implemented our framework with Scribble-Go, a tool chain for programming such role-parametric protocols in the mainstream programming language of Go. We generate API families of lightweight, protocol- and variant-specific type wrappers for I/O. The API ensures a well-typed Go endpoint program (by native Go type checking) will perform only the compliant I/O actions wrt to the source protocol. We leverage the abstractions of MPST to support the specification of Go applications involving multiple channels, possibly over mixed transport, and channel passing via a unified programming interface. We evaluate the applicability and runt-time performance of our generated API using microbenchmarks and real-world applications.

Date 27 Sep 2018
Speakers
Effpi; Concurrent Programming with Dependent Behavioural Types
VeTSS/FMATS6

Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.

I will talk about Effpi, a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. Scala 3). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.

The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types (from the π-calculus theory), and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving program thunks). This design has three main advantages. First, it allows to verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes/actors.

Date 25 Sep 2018
Speakers
Effpi; Concurrent Programming with Dependent Behavioural Types
University of Novi Sad, Serbia

Concurrent and distributed programming is notoriously hard. Many languages and software toolkits address the challenge by offering high-level abstractions, such as message-passing processes and actors; they allow for intuitive reasoning, but do not formally ensure that a program implements a given specification.

I will talk about Effpi, a toolkit for strongly-typed concurrent programming in Dotty (a.k.a. Scala 3). Effpi allows to specify the intended behaviour of a message-passing application using types: i.e., if a program type-checks and compiles, then it will run and communicate as prescribed by its types.

The foundation of Effpi is a concurrent functional language with a novel blend of behavioural types (from the π-calculus theory), and a form of dependent types, extending to higher-order interaction (i.e., sending/receiving program thunks). This design has three main advantages. First, it allows to verify programs through a combination of type checking and model checking techniques. Second, it is directly implemented (via deep embedding) in Dotty, including a simplified API for strongly-typed actor-based programming. And third, its functional nature allows for an efficient runtime system, supporting highly concurrent programs with millions of interacting processes/actors.

Date 17 Sep 2018
Speakers
Reversibility between Polymorphic Sessions and Functions
ICT COST Action IC1405 meeting, Leicester, UK
Date 10 Sep 2018
Speakers
Behavioural Type-Based Static Verification Framework for Go
TRENDS 2018 invited talk, Beijing, China

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks. In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

Date 8 Sep 2018
Speakers
On Polymorphic Sessions and Functions
Department Seminar, University of Nagoya, Japan

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Date 7 Aug 2018
Speakers
On Polymorphic Sessions and Functions
National Institute of Informatics, Tokyo, Japan

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Date 24 Jul 2018
Speakers
Compile-time Generation of Session Types with Interaction Refinements
FLOLAC 2018, Taiwan

We first give an overview of recent research developments of our mobility group at Imperial College London.

Session types is a typing discipline for concurrent and distributed processes that allows errors such as communication mismatches and deadlocks to be detected statically. Refinement types are types elaborated by logical constraints that allow richer and finer-grained specification of application properties, combining types with logical formulae that may refer to program values and can constrain types using arbitrary predicates. Type providers, developed in F#, are compile-time components for on-demand code generation. Their architecture relies on an open-compiler, where provider-authors implement a small interface that allows them to inject new names/types into the programming context as the program is written.

In this talk, we will present a library that integrates aspects from the above fields to realise practical applications of multiparty refinement session types (MPST) for any .Net language. Our library supports the specification and validation of distributed message passing protocols based on a formulation of asynchronous MPST enriched with interaction refinements: a collection of features related to the refinement of protocols, such as message-type refinements (value constraints) and value dependent control flow. The combination of these aspects—session types for structured interactions, constraint solving from refinement types, and protocol-specific code generation—enables the specification and implementation of enriched protocols in native F# (and any .Net-compiled language) without requiring language extensions or external pre-processing of user programs. A well-typed endpoint program using our library is guaranteed to perform only compliant session I/O actions w.r.t. to the refined protocol, up to premature termination. The safety guarantees are achieved by a combination of static type checking of the generated types for messages and I/O operations, correctness by construction from code generation, and automated inlining of assertions.

Date 19 Jul 2018
Speakers
Behavioural Type-based Static Verification Framework for Go
Programming Languages and Systems group seminar, University of Kent, UK

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

(joint work with Julien Lange, Bernardo Toninho and Nobuko Yoshida)

Date 21 May 2018
Speakers
Behavioural Type-Based Static Verification Framework for Go
Department of Computer Science, University of Cyprus, Cyprus

Go is a production-level statically typed programming language whose design features explicit message-passing primitives and lightweight threads, enabling (and encouraging) programmers to develop concurrent systems where components interact through communication more so than by lock-based shared memory concurrency. Go can detect global deadlocks at runtime, but does not provide any compile-time protection against all too common communication mismatches and partial deadlocks.

In this work we present a static verification framework for liveness and safety in Go programs, able to detect communication errors and deadlocks by model checking. Our toolchain infers from a Go program a faithful representation of its communication patterns as behavioural types, where the types are model checked for liveness and safety.

This is joint work with Julien Lange (Kent), Bernardo Toninho (Imperial) and Nicholas Ng (Imperial).

Date 14 May 2018
Speakers
On Polymorphic Sessions and Functions
ESOP 2018, Thessaloniki, Greece

This work exploits the logical foundation of session types to determine what kind of type discipline for the π-calculus can exactly capture, and is captured by, λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

Date 19 Apr 2018
Speakers
Non-angelic concurrent game semantics
FOSSACS 2018, Thessaloniki, Greece

The hiding operation, crucial in the construction of categories of games and strategies and hence the compositional aspect of game semantics, has a tendency, as a side effect, to remove branches of computation not leading to observable results. Accordingly, games models of programming languages are usually biased towards angelic non-determinism, where branches leading to e.g. divergence are forgotten. We present here new categories of games, which do not suffer from this bias. In our first category, we achieve this by avoiding hiding altogether; instead morphisms are uncovered strategies (with neutral/invisible events) up to weak bisimulation. Then, we show that by hiding only certain events dubbed inessential we can consider strategies up to isomorphism, and still get a category – this partial hiding remains sound up to weak bisimulation, so we get a concrete representations of morphisms (as in standard concurrent games) while avoiding the angelic bias. We give a semantics for Affine Idealized Parallel Algol which is adequate for both may and must equivalence within the model

Date 16 Apr 2018
Speakers
Earlier