Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 17:21 - 17:43 at Sala II - Session Types II Chair(s): Andrew D. Gordon

Multiparty Session Types (MPST) are a typing discipline ensuring that a message-passing process implements a given multiparty session protocol, without errors. In this paper, we propose a new, generalised MPST theory.

Our contribution is fourfold.

  1. We demonstrate that a revision of the theoretical foundations of MPST is necessary: classic MPST have a limited subject reduction property, with inherent restrictions that are easily overlooked, and in previous work have led to flawed type safety proofs; our new theory removes such restrictions and fixes such flaws.

  2. We contribute a new MPST theory that is less complicated, and yet more general, than the classic one: it does not require global multiparty session types nor binary session type duality — instead, it is grounded on general behavioural type-level properties, and proves type safety of many more protocols and processes.

  3. We produce a detailed analysis of type-level properties, showing how, in our new theory, they allow to ensure decidability of type checking, and statically guarantee that processes enjoy, e.g., deadlock-freedom and liveness at run-time.

  4. We show how our new theory can integrate type and model checking: type-level properties can be expressed in modal μ-calculus, and verified with well-established tools.

Slides (popl19-slides.pdf)1.74MiB

Wed 16 Jan

POPL-2019-Research-Papers
16:37 - 17:43: Research Papers - Session Types II at Sala II
Chair(s): Andrew D. GordonMicrosoft Research and University of Edinburgh
POPL-2019-Research-Papers16:37 - 16:59
Talk
Bernardo ToninhoImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached
POPL-2019-Research-Papers16:59 - 17:21
Talk
David CastroImperial College London, Raymond HuImperial College London, Sung-Shik JongmansOpen University of the Netherlands, Nicholas NgImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached File Attached
POPL-2019-Research-Papers17:21 - 17:43
Talk
Alceste ScalasImperial College London, Nobuko YoshidaImperial College London
Link to publication DOI Pre-print Media Attached File Attached