Dependent Session Types

Session types offer a type-based discipline for enforcing communication protocols in distributed programming. We have previously formalized simple session types in the setting of multi-threaded $λ$-calculus with linear types. In this work, we build upon our earlier work by presenting a form of depen...

Full description

Bibliographic Details
Main Authors: Wu, Hanwen, Xi, Hongwei
Format: Report
Language:unknown
Published: arXiv 2017
Subjects:
Programming Languages cs.PL
Distributed, Parallel, and Cluster Computing cs.DC
FOS Computer and information sciences
F.1.2; F.4.1
DML
Online Access:https://dx.doi.org/10.48550/arxiv.1704.07004
https://arxiv.org/abs/1704.07004
id ftdatacite:10.48550/arxiv.1704.07004
record_format openpolar
spelling ftdatacite:10.48550/arxiv.1704.07004 2023-05-15T16:01:49+02:00 Dependent Session Types Wu, Hanwen Xi, Hongwei 2017 https://dx.doi.org/10.48550/arxiv.1704.07004 https://arxiv.org/abs/1704.07004 unknown arXiv Creative Commons Attribution 4.0 International https://creativecommons.org/licenses/by/4.0/legalcode cc-by-4.0 CC-BY Programming Languages cs.PL Distributed, Parallel, and Cluster Computing cs.DC FOS Computer and information sciences F.1.2; F.4.1 Preprint Article article CreativeWork 2017 ftdatacite https://doi.org/10.48550/arxiv.1704.07004 2022-04-01T10:47:44Z Session types offer a type-based discipline for enforcing communication protocols in distributed programming. We have previously formalized simple session types in the setting of multi-threaded $λ$-calculus with linear types. In this work, we build upon our earlier work by presenting a form of dependent session types (of DML-style). The type system we formulate provides linearity and duality guarantees with no need for any runtime checks or special encodings. Our formulation of dependent session types is the first of its kind, and it is particularly suitable for practical implementation. As an example, we describe one implementation written in ATS that compiles to an Erlang/Elixir back-end. Report DML DataCite Metadata Store (German National Library of Science and Technology)
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
Distributed, Parallel, and Cluster Computing cs.DC
FOS Computer and information sciences
F.1.2; F.4.1
spellingShingle Programming Languages cs.PL
Distributed, Parallel, and Cluster Computing cs.DC
FOS Computer and information sciences
F.1.2; F.4.1
Wu, Hanwen
Xi, Hongwei
Dependent Session Types
topic_facet Programming Languages cs.PL
Distributed, Parallel, and Cluster Computing cs.DC
FOS Computer and information sciences
F.1.2; F.4.1
description Session types offer a type-based discipline for enforcing communication protocols in distributed programming. We have previously formalized simple session types in the setting of multi-threaded $λ$-calculus with linear types. In this work, we build upon our earlier work by presenting a form of dependent session types (of DML-style). The type system we formulate provides linearity and duality guarantees with no need for any runtime checks or special encodings. Our formulation of dependent session types is the first of its kind, and it is particularly suitable for practical implementation. As an example, we describe one implementation written in ATS that compiles to an Erlang/Elixir back-end.
format Report
author Wu, Hanwen
Xi, Hongwei
author_facet Wu, Hanwen
Xi, Hongwei
author_sort Wu, Hanwen
title Dependent Session Types
title_short Dependent Session Types
title_full Dependent Session Types
title_fullStr Dependent Session Types
title_full_unstemmed Dependent Session Types
title_sort dependent session types
publisher arXiv
publishDate 2017
url https://dx.doi.org/10.48550/arxiv.1704.07004
https://arxiv.org/abs/1704.07004
genre DML
genre_facet DML
op_rights Creative Commons Attribution 4.0 International
https://creativecommons.org/licenses/by/4.0/legalcode
cc-by-4.0
op_rightsnorm CC-BY
op_doi https://doi.org/10.48550/arxiv.1704.07004
_version_ 1766397528766414848

Similar Items