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: | Text |
Language: | unknown |
Published: |
2016
|
Subjects: | |
Online Access: | http://arxiv.org/abs/1604.03020 |
id |
ftarxivpreprints:oai:arXiv.org:1604.03020 |
---|---|
record_format |
openpolar |
spelling |
ftarxivpreprints:oai:arXiv.org:1604.03020 2023-09-05T13:19:06+02:00 Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions Xi, Hongwei Wu, Hanwen 2016-04-11 http://arxiv.org/abs/1604.03020 unknown http://arxiv.org/abs/1604.03020 Computer Science - Programming Languages text 2016 ftarxivpreprints 2023-08-16T13:58:06Z 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. Comment: 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 Text DML ArXiv.org (Cornell University Library) Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
ArXiv.org (Cornell University Library) |
op_collection_id |
ftarxivpreprints |
language |
unknown |
topic |
Computer Science - Programming Languages |
spellingShingle |
Computer Science - Programming Languages Xi, Hongwei Wu, Hanwen Linearly Typed Dyadic Group Sessions for Building Multiparty Sessions |
topic_facet |
Computer Science - Programming Languages |
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. Comment: 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 |
Text |
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 |
publishDate |
2016 |
url |
http://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_relation |
http://arxiv.org/abs/1604.03020 |
_version_ |
1776199924691501056 |