Multiparty symmetric sum types
File(s)DTR09-8.pdf (298.19 KB)
Published version
Author(s)
Yoshida, Nobuko
Nielsen, Lasse
Honda, Johei
Type
Report
Abstract
This paper extends the multiparty asynchronous session types to symmetric sumtypes, which can
type non-deterministic orchestration choice behaviours. While the original branching in the session
types requires one participant to decide how to proceed by sending a label, with symmetric sumtypes
the choice can be made in a non-deterministic way by synchronisation between the participants in a
multiparty session. The motivation for synchronisation comes from natural and concise modelling
of social interaction and cooperation in healthcare scenarios in the Process Matrix. The behaviour of
synchronisation is represented by a new synchronise process constructor, which is typed by symmetric
sumtypes. Finally we show that symmetric sumtypes can be erased into the original branching
types with the help of conductor processes, preserving typability and operational semantics.
type non-deterministic orchestration choice behaviours. While the original branching in the session
types requires one participant to decide how to proceed by sending a label, with symmetric sumtypes
the choice can be made in a non-deterministic way by synchronisation between the participants in a
multiparty session. The motivation for synchronisation comes from natural and concise modelling
of social interaction and cooperation in healthcare scenarios in the Process Matrix. The behaviour of
synchronisation is represented by a new synchronise process constructor, which is typed by symmetric
sumtypes. Finally we show that symmetric sumtypes can be erased into the original branching
types with the help of conductor processes, preserving typability and operational semantics.
Date Issued
2009-01-01
Citation
Departmental Technical Report: 09/8, 2009, pp.1-23
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
23
Journal / Book Title
Departmental Technical Report: 09/8
Copyright Statement
© 2009 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
09/8