MobilityReadingGroup

π-calculus, Session Types research at Imperial College

Talks & Presentations

Recent invited talks and presentations from our group.

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
Session Types and Game Semantics Synchrony and Asynchrony
GaLoP 2018, Thessaloniki, Greece
Date 14 Apr 2018
Speakers
Behavioural Type-Based Static Verification Framework for Go
ICT Seminar, Western Norway University of Applied Sciences, Norway

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 and Bernardo Toninho

Date 12 Mar 2018
Speakers
Reversible Event Structures
Guest talk at Programming, Logic and Semantics Research Group, IT University of Copenhagen, Denmark

We first talk about a summary of recent activities in Mobility Session Type Group in Imperial College London. Then we talk about the main technical topic.

Event structures have been used for modelling forward-only process calculi. We define (categories of) reversible variants of prime, asymmetric, bundle, extended bundle, and general event structures for the purpose of using one of these variants to define truly concurrent semantics of reversible process calculi. We use the causal subcategory of reversible bundle event structures to define semantics of, CCSK, a reversible variant of CCS. We also expand CCSK to control the reversibility using a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we use extended bundle event structures, which add asymmetric conflict to bundle event structures, and use their capacity for non-causal reversibility.

Date 8 Mar 2018
Speakers
Behavioural Type-Based Static Verification Framework for Go
Computer Science Seminar Series, University of Camerino, Italy

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 7 Dec 2017
Speakers
Linear Logic and Session Types
Mathematical Foundataions Seminars, University of Bath, UK

In this talk, we first outline recent activities in our mobility group in Department of Computing, Imperial College London.

Then we talk about the following work on Linear Logic and Session Types.

Linear logic has long been heralded as a potential model for concurrency: from Girard’s original paper, to Abramsky’s computational interpretation, reiterated by Bellin and Scott. More recently, an interpretation for intuitionistic linear logic has been given by Caires and Pfenning where propositions are viewed as session types - a well established typing discipline for concurrency - proofs as processes and proof reduction as inter-process communication.

In this talk we will detail how several generalisations and extensions of this interpretation arguably form a basis for a logical foundation that captures several interesting features of message-passing concurrent computation. Specifically, we will detail how the basic interpretation can be extended to richer typed settings such as polymorphism and dependent type theories and how to account for a meaningful notion of typed process equivalence that gives meaning to both proof conversions and type isomorphisms.

Date 28 Nov 2017
Speakers
The parallel intensionally fully abstract model for PCF
IRIF, Université Paris-Diderot, France

In this talk, we introduce a new game semantics framework for concurrency based on event structures, extending the work of Rideau and Winskel. In this framework, we can extend the notions of innocence and well-bracketing to the concurrent (and non-deterministic) case, generalizing the so-called “Abramsky cube”.

This talk focuses on the deterministic case. I will first introduce the concurrent strategies and their composition, in the existing linear setting. I will then present our extension to nonlinearity using copy indices and symmetry to represent uniformity. I will then present our notions of concurrent innocence & well-bracketing, to finish on our result of intensional full abstraction for PCF. Time permitting, I will discuss extensions of this result to non-angelic nondeterminism and probabilities.

Date 23 Nov 2017
Speakers
Towards a causal and compositional operational semantics of programming languages
LSV, ENS Paris-Saclay, France

In this talk, I will present methods and mathematical tools to give operational, yet compositional, causal models of programming languages, using Winskel’s event structures. We first illustrate the methodology on a first-order concurrent programming language, in the setting of weak memory models where causal models turn out to be handy to understand cleanly reorderings operated by the hardware.

We then turn to higher-order languages, such as the π-calculus and the λ-calculus. We show how name binding can be elegantly expressed in the semantics by means of game semantics. Types, seen as protocols, become games, and (open) programs become strategies. From there, we can build a cartesian-closed category that supports interpretation of higher-order concurrent and nondeterministic computations. We show we can support interpretations sound and adequate for to may, must and fair convergences, using essential events (unobservable events keeping track of nondeterministic choices).

Date 21 Nov 2017
Speakers
Behavioural Type-Based Static Verification Framework for Go
A Shared Challenge in Behavioural Specification (Dagstuhl Seminar 17462), Schloss Dagstuhl, Germany, November 2017

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 12 Nov 2017 - 15 Nov 2017
Speakers
Scala, an overview
Programming Languages Reading Group, DoCSoc, Imperial College

I will give a brief overview of the Scala programming language, highlighting some similarities and differences with respect to Java and Haskell. I will also mention how the Mobility Reading Group at Imperial College London uses Scala for its research on type-safe concurrent and distributed applications

Date 31 Oct 2017
Speakers
Session Types as a Descriptive Tool for Distributed Protocols
EECS Distinguished Lecture Seminar, Queen Mary, University of London

We give a summary of our recent research developments on multiparty session types for verifying distributed, parallel and concurrent programs, and our collaborations with industry partners. We shall first talk how the session types were discovered from the theory of the pi-calculus by Kohei Honda, and how we started collaborations with industry to develop a protocol description language called Scribble. We then talk about the recent developments in Scribble, the network protocol verifications with demos.

Date 25 Oct 2017
Speakers
Mario and Mariangiola's Contribution to the Session Type Theory and Practice
Types and Logic in Torino, Colloquium in honor of Mariangiola Dezani-Ciancaglini, Simona Ronchi Della Rocca and Mario Coppo

Since the year 2000, Mario and Mariangiola’s research has been devoted to the study of session types for ensuring safety and liveness of communication protocols. Mariangiola first proposed a formalisation of Java with session types and later it was extended to asynchronous communications with Mario, which was later applied to the design and implementation of Session Java (SJ). These contributions initiated a flurry of research activity aiming at applying session types to many real-world programming languages. Mariangiola first studied a theory of progress in the session types for the pi-calculus, whose core theory was later extended with Mario to multiparty session types. This formalism became the core of the current version of an open-source protocol description language, Scribble, which is developed at Red Hat and Imperial. The Scribble language is used in the multi-million-USD Ocean Observatory Initiative project. I will talk about how their elegant works give the practical impacts to communication-intensive programming frameworks.

Date 22 Sep 2017
Speakers
Let it Recover: Multiparty Protocol-Induced Recovery
ICT COST Action IC 1405 meeting, Faculty of Mathematics and Computer Science of Nicolaus Copernicus University in Toruń, Poland
Date 1 Sep 2017 - 2 Sep 2017
Speakers
Understanding concurrency with behavioural types
GolangUK 2017, 16-18 Aug 2017

Concurrent programming is difficult. This talk is about applying programming languages & concurrency research, specifically behavioural types as an abstraction, to verify concurrent Go programs. The talk covers what behavioural types are and how they can be used to reason in Go’s concurrency model.

Date 16 Aug 2017 - 18 Aug 2017
Speakers
Let it Recover: Multiparty Protocol-Induced Recovery
Open Problems in Concurrency Theory II, Institute of Science of Technology Austria (IST Austria), Vienna
Date 26 Jun 2017 - 29 Jun 2017
Speakers
Open problems in session types
Open Problems in Concurrency Theory II, Institute of Science of Technology Austria (IST Austria), Vienna
Date 26 Jun 2017 - 29 Jun 2017
Speakers
Behavioural Type-Based Static Verification Framework for Go
HKU PL Group, The University of Hong Kong, Hong Kong, June 2017

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, Bernardo Toninho, and Nobuko Yoshida.

Date 9 Jun 2017
Speakers
Earlier