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: | Report |
Language: | unknown |
Published: |
arXiv
2016
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.1604.03020 https://arxiv.org/abs/1604.03020 |
id |
ftdatacite:10.48550/arxiv.1604.03020 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.48550/arxiv.1604.03020 2023-05-15T16:02:00+02:00 Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions Xi, Hongwei Wu, Hanwen 2016 https://dx.doi.org/10.48550/arxiv.1604.03020 https://arxiv.org/abs/1604.03020 unknown arXiv arXiv.org perpetual, non-exclusive license http://arxiv.org/licenses/nonexclusive-distrib/1.0/ Programming Languages cs.PL FOS Computer and information sciences Preprint Article article CreativeWork 2016 ftdatacite https://doi.org/10.48550/arxiv.1604.03020 2022-04-01T11:34:18Z 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. : This paper can be seen as the pre-sequel to classical linear multirole logic (CLML). arXiv admin note: substantial text overlap with arXiv:1603.03727 Report DML DataCite Metadata Store (German National Library of Science and Technology) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
DataCite Metadata Store (German National Library of Science and Technology) |
op_collection_id |
ftdatacite |
language |
unknown |
topic |
Programming Languages cs.PL FOS Computer and information sciences |
spellingShingle |
Programming Languages cs.PL FOS Computer and information sciences Xi, Hongwei Wu, Hanwen Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions |
topic_facet |
Programming Languages cs.PL FOS Computer and information sciences |
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. : This paper can be seen as the pre-sequel to classical linear multirole logic (CLML). arXiv admin note: substantial text overlap with arXiv:1603.03727 |
format |
Report |
author |
Xi, Hongwei Wu, Hanwen |
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 |
publisher |
arXiv |
publishDate |
2016 |
url |
https://dx.doi.org/10.48550/arxiv.1604.03020 https://arxiv.org/abs/1604.03020 |
long_lat |
ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
geographic |
Lambda |
geographic_facet |
Lambda |
genre |
DML |
genre_facet |
DML |
op_rights |
arXiv.org perpetual, non-exclusive license http://arxiv.org/licenses/nonexclusive-distrib/1.0/ |
op_doi |
https://doi.org/10.48550/arxiv.1604.03020 |
_version_ |
1766397644730531840 |