Parameterised Session Types Communication Patterns: Through the Looking Glass of Session Types
Author(s)
Bejleri, Andi
Type
Thesis or dissertation
Abstract
This dissertation studies a type theory to guarantee communication-safety in sessions of
an arbitrary number of participants, typically represented as communication patterns,
of mobile processes in the context of multiparty session types— a well-established type
theory that describes the interactive structure of a fixed number of processes from a global
point of view and type-checks the processes through projection of the global type onto the
participants of the session. Communication-safety is the property that mobile processes
exchange values of the same set without deadlocking and data races.
Our study introduces a programming idiom of roles— a concept that describes the
nature of a communication pattern in a similar way to classes in Java and C#, offering a
design on how to incorporate parameterised session types into a mainstream language. The
formal model (1) preserves multiparty session types’ syntax and type-checking strategy,
and (2) allows the number of participants to range over infinite sets of natural numbers,
providing full computation power of programs. A series of communication patterns and
real-world examples from parallel algorithms and data exchange protocols demonstrate
the expressiveness and practicality of the formal model, comparing the model with the
only mature implementation of (binary) session types. We proved that type preservation
under reduction and communication-safety hold in the type system.
The study of parameterised session types is supported by the examination of multiparty
session types for synchronous communications. We extended the initial work on multiparty
session types with a simpler calculus, multicast send of values and labels, a practical form
of higher-order communication and a more intuitive, elegant linearity property; we proved
that (a) type preservation and communication-safety hold in the type system, and (b)
interactions of a typeable process follow exactly the description of the global type.
an arbitrary number of participants, typically represented as communication patterns,
of mobile processes in the context of multiparty session types— a well-established type
theory that describes the interactive structure of a fixed number of processes from a global
point of view and type-checks the processes through projection of the global type onto the
participants of the session. Communication-safety is the property that mobile processes
exchange values of the same set without deadlocking and data races.
Our study introduces a programming idiom of roles— a concept that describes the
nature of a communication pattern in a similar way to classes in Java and C#, offering a
design on how to incorporate parameterised session types into a mainstream language. The
formal model (1) preserves multiparty session types’ syntax and type-checking strategy,
and (2) allows the number of participants to range over infinite sets of natural numbers,
providing full computation power of programs. A series of communication patterns and
real-world examples from parallel algorithms and data exchange protocols demonstrate
the expressiveness and practicality of the formal model, comparing the model with the
only mature implementation of (binary) session types. We proved that type preservation
under reduction and communication-safety hold in the type system.
The study of parameterised session types is supported by the examination of multiparty
session types for synchronous communications. We extended the initial work on multiparty
session types with a simpler calculus, multicast send of values and labels, a practical form
of higher-order communication and a more intuitive, elegant linearity property; we proved
that (a) type preservation and communication-safety hold in the type system, and (b)
interactions of a typeable process follow exactly the description of the global type.
Date Issued
2012-02
Online Publication Date
2012-03-23T10:59:51Z
Date Awarded
2012-03
Advisor
Yoshida, Nobuko
Sponsor
EPSRC
Creator
Bejleri, Andi
Grant Number
EP/F003757/1 and EP/T03215/01.
Publisher Department
Computing
Publisher Institution
Imperial College London
Qualification Level
Doctoral
Qualification Name
Doctor of Philosophy (PhD)