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: | Article in Journal/Newspaper |
Language: | English |
Published: |
2016
|
Subjects: | |
Online Access: | https://hdl.handle.net/2144/45002 http://arxiv.org/abs/1603.03727v1 |
id |
ftbostonuniv:oai:open.bu.edu:2144/45002 |
---|---|
record_format |
openpolar |
spelling |
ftbostonuniv:oai:open.bu.edu:2144/45002 2023-05-15T16:01:56+02:00 Session types in a linearly typed multi-threaded lambda-calculus Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William 2016-03-11 https://hdl.handle.net/2144/45002 http://arxiv.org/abs/1603.03727v1 en_US eng http://arxiv.org/abs/1603.03727v1 H. Xi, Z. Ren, H. Wu, W. Blair. 2016. "Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus." https://arxiv.org/abs/1603.03727 https://hdl.handle.net/2144/45002 188567 Article 2016 ftbostonuniv 2022-08-20T22:18:13Z 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. First author draft Article in Journal/Newspaper DML Boston University: OpenBU Lambda ENVELOPE(-62.983,-62.983,-64.300,-64.300) |
institution |
Open Polar |
collection |
Boston University: OpenBU |
op_collection_id |
ftbostonuniv |
language |
English |
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. First author draft |
format |
Article in Journal/Newspaper |
author |
Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William |
spellingShingle |
Xi, Hongwei Ren, Zhiqiang Wu, Hanwen Blair, William Session types in a linearly typed multi-threaded lambda-calculus |
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 |
https://hdl.handle.net/2144/45002 http://arxiv.org/abs/1603.03727v1 |
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.03727v1 H. Xi, Z. Ren, H. Wu, W. Blair. 2016. "Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus." https://arxiv.org/abs/1603.03727 https://hdl.handle.net/2144/45002 188567 |
_version_ |
1766397606229966848 |