Session Types in a Linearly Typed Multi-Threaded Lambda-Calculus

• Main Authors: Xi, Hongwei, Ren, Zhiqiang, Wu, Hanwen, Blair, William
• Format: Report
• Language: unknown
• Published: arXiv 2016
• Subjects: Programming Languages cs.PL; Logic in Computer Science cs.LO; FOS Computer and information sciences; Lambda; DML
• Online Access: https://dx.doi.org/10.48550/arxiv.1603.03727; https://arxiv.org/abs/1603.03727

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...