MobilityReadingGroup

π-calculus, Session Types research at Imperial College

News: Kohei Honda's paper awarded the ETAPS 2019 Test-of-Time Award
11 Apr 2019

The paper ‘Language primitives and type discipline for structured communication-based programming’ by Kohei Honda, Vasco T. Vasconcelos and Makoto Kubo, has received the ETAPS 2019 Test-of-Time Award.

The citation for the paper:

This is one of the seminal papers on session types. Session types are type-theoretic specifications of communication protocols, allowing protocol implementations to be verified by static type-checking. During the last 20 years, the research topic of session types has grown steadily, and has been applied to programming languages including Haskell, OCaml, Java, Python and Go. Connections have been made to software contracts, model-checking, logic, runtime verification and hardware specification. Session types regularly feature at major programming language conferences: for example, there are 5 papers on session types at ETAPS 2018. Session types have formed the basis for numerous funded research projects, including COST Action IC1201 (www.behavioural-types.eu), a network of more than 120 researchers in 22 countries.

This is the paper that is most frequently read and cited (832 in Google Scholar, up from 749 last year) as an original reference for session types. It made two key advances with respect to earlier papers by Honda et al. First, it covered the whole of pi-calculus by introducing delegation, which is the ability to transfer a session as a communication channel, from one process to another, so that the receiver continues the protocol started by the sender. Second, it included a broad range of examples of the use of session types - functional programming, concurrent objects, and network protocols - thus anticipating implementations and applications of session types that are now widely used.

ETAPS 2019 Test-of-Time Award

Relive the award ceremony: