Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus
We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reac...
Main Authors: | , , , |
---|---|
Format: | Report |
Language: | unknown |
Published: |
arXiv
2016
|
Subjects: | |
Online Access: | https://dx.doi.org/10.48550/arxiv.1603.03727 https://arxiv.org/abs/1603.03727 |
id |
ftdatacite:10.48550/arxiv.1603.03727 |
---|---|
record_format |
openpolar |
spelling |
ftdatacite:10.48550/arxiv.1603.03727 2023-05-15T16:01:58+02:00 Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William 2016 https://dx.doi.org/10.48550/arxiv.1603.03727 https://arxiv.org/abs/1603.03727 unknown arXiv arXiv.org perpetual, non-exclusive license http://arxiv.org/licenses/nonexclusive-distrib/1.0/ Programming Languages cs.PL Logic in Computer Science cs.LO FOS Computer and information sciences Preprint Article article CreativeWork 2016 ftdatacite https://doi.org/10.48550/arxiv.1603.03727 2022-04-01T11:34:18Z We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reach a deadlock. 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 session types in ATS. In addition, we gain immediate support for a form of dependent session types based on this embedding into ATS. Compared to various existing formalizations of session types, we see the one given in this paper is unique in its closeness to concrete implementation. In particular, we report such an implementation ready for practical use that generates Erlang code from well-typed ATS source (making use of session types), thus taking great advantage of the infrastructural support for distributed computing in Erlang. : This is the original version of the paper on supporting programming with dyadic session types in ATS 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 Logic in Computer Science cs.LO FOS Computer and information sciences |
spellingShingle |
Programming Languages cs.PL Logic in Computer Science cs.LO FOS Computer and information sciences Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
topic_facet |
Programming Languages cs.PL Logic in Computer Science cs.LO FOS Computer and information sciences |
description |
We present a formalization of session types in a multi-threaded lambda-calculus (MTLC) equipped with a linear type system, establishing for the MTLC both type preservation and global progress. The latter (global progress) implies that the evaluation of a well-typed program in the MTLC can never reach a deadlock. 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 session types in ATS. In addition, we gain immediate support for a form of dependent session types based on this embedding into ATS. Compared to various existing formalizations of session types, we see the one given in this paper is unique in its closeness to concrete implementation. In particular, we report such an implementation ready for practical use that generates Erlang code from well-typed ATS source (making use of session types), thus taking great advantage of the infrastructural support for distributed computing in Erlang. : This is the original version of the paper on supporting programming with dyadic session types in ATS |
format |
Report |
author |
Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William |
author_facet |
Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William |
author_sort |
Xi, Hongwei |
title |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
title_short |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
title_full |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
title_fullStr |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
title_full_unstemmed |
Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
title_sort |
session types in a linearly typed multi-threaded lambda-calculus |
publisher |
arXiv |
publishDate |
2016 |
url |
https://dx.doi.org/10.48550/arxiv.1603.03727 https://arxiv.org/abs/1603.03727 |
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.1603.03727 |
_version_ |
1766397624933416960 |