Linearly typed dyadic group sessions for building multiparty sessions
Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implemen...
Main Authors: | , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
2016
|
Subjects: | |
Online Access: | https://hdl.handle.net/2144/45001 http://arxiv.org/abs/1604.03020v1 |
id |
ftbostonuniv:oai:open.bu.edu:2144/45001 |
---|---|
record_format |
openpolar |
spelling |
ftbostonuniv:oai:open.bu.edu:2144/45001 2023-05-15T16:01:58+02:00 Linearly typed dyadic group sessions for building multiparty sessions Xi, Hongwei Wu, Hanwen 2016-04-11 https://hdl.handle.net/2144/45001 http://arxiv.org/abs/1604.03020v1 en_US eng http://arxiv.org/abs/1604.03020v1 H. Xi, H. Wu. 2016. "Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions." https://arxiv.org/abs/1604.03020 https://hdl.handle.net/2144/45001 188557 Article 2016 ftbostonuniv 2022-08-20T22:18:13Z Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implement a group of roles based on one channel. In particular, each of the two parties involved in a dyadic g-session implements either a group of roles or its complement. In this paper, we present a formalization of g-sessions in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of linearly typed g-sessions in ATS. The primary contribution of the paper lies in both of the identification of g-sessions as a fundamental building block for multiparty sessions and the theoretical development in support of this identification. First author draft Article in Journal/Newspaper DML Boston University: OpenBU Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
Boston University: OpenBU |
op_collection_id |
ftbostonuniv |
language |
English |
description |
Traditionally, each party in a (dyadic or multiparty) session implements exactly one role specified in the type of the session. We refer to this kind of session as an individual session (i-session). As a generalization of i-session, a group session (g-session) is one in which each party may implement a group of roles based on one channel. In particular, each of the two parties involved in a dyadic g-session implements either a group of roles or its complement. In this paper, we present a formalization of g-sessions in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. As this formulated MTLC can be readily embedded into ATS, a full-fledged language with a functional programming core that supports both dependent types (of DML-style) and linear types, we obtain a direct implementation of linearly typed g-sessions in ATS. The primary contribution of the paper lies in both of the identification of g-sessions as a fundamental building block for multiparty sessions and the theoretical development in support of this identification. First author draft |
format |
Article in Journal/Newspaper |
author |
Xi, Hongwei Wu, Hanwen |
spellingShingle |
Xi, Hongwei Wu, Hanwen Linearly typed dyadic group sessions for building multiparty sessions |
author_facet |
Xi, Hongwei Wu, Hanwen |
author_sort |
Xi, Hongwei |
title |
Linearly typed dyadic group sessions for building multiparty sessions |
title_short |
Linearly typed dyadic group sessions for building multiparty sessions |
title_full |
Linearly typed dyadic group sessions for building multiparty sessions |
title_fullStr |
Linearly typed dyadic group sessions for building multiparty sessions |
title_full_unstemmed |
Linearly typed dyadic group sessions for building multiparty sessions |
title_sort |
linearly typed dyadic group sessions for building multiparty sessions |
publishDate |
2016 |
url |
https://hdl.handle.net/2144/45001 http://arxiv.org/abs/1604.03020v1 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
DML |
genre_facet |
DML |
op_relation |
http://arxiv.org/abs/1604.03020v1 H. Xi, H. Wu. 2016. "Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions." https://arxiv.org/abs/1604.03020 https://hdl.handle.net/2144/45001 188557 |
_version_ |
1766397623452827648 |