Session types in a linearly typed multi-threaded lambda-calculus
Files
First author draft
Date
2016-03-11
DOI
Authors
Xi, Hongwei
Ren, Zhiqiang
Wu, Hanwen
Blair, William
Version
First author draft
OA Version
Citation
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
Abstract
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.