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: | Text |
Language: | unknown |
Published: |
2016
|
Subjects: | |
Online Access: | http://arxiv.org/abs/1603.03727 |
id |
ftarxivpreprints:oai:arXiv.org:1603.03727 |
---|---|
record_format |
openpolar |
spelling |
ftarxivpreprints:oai:arXiv.org:1603.03727 2023-09-05T13:19:06+02:00 Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William 2016-03-11 http://arxiv.org/abs/1603.03727 unknown http://arxiv.org/abs/1603.03727 Computer Science - Programming Languages Computer Science - Logic in Computer Science text 2016 ftarxivpreprints 2023-08-16T13:56:19Z 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. Comment: This is the original version of the paper on supporting programming with dyadic session types in ATS 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 Computer Science - Logic in Computer Science |
spellingShingle |
Computer Science - Programming Languages Computer Science - Logic in Computer Science Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus |
topic_facet |
Computer Science - Programming Languages Computer Science - Logic in Computer Science |
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. Comment: This is the original version of the paper on supporting programming with dyadic session types in ATS |
format |
Text |
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 |
publishDate |
2016 |
url |
http://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_relation |
http://arxiv.org/abs/1603.03727 |
_version_ |
1776199924022509568 |