A Session Type System with Subject Reduction

Keigo IMAI  Shoji YUEN  Kiyoshi AGUSA  

IEICE TRANSACTIONS on Information and Systems   Vol.E95-D   No.8   pp.2053-2064
Publication Date: 2012/08/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.E95.D.2053
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Software System
Pi-calculus,  session types,  type system,  subject reduction,  concurrency,  process calculi,  polarity,  

Full Text: PDF>>
Buy this Article

Distributed applications and services have become pervasive in our society due to the widespread use of internet and mobile devices. There are urgent demands to efficiently ensure safety and correctness of such software. A session-type system is a framework to statically check whether communication descriptions conform to certain protocols. They are shown to be effective yet simple enough to fit in harmony with existing programming languages. In the original session type system, the subject reduction property does not hold. This paper establishes a conservative extension of the original session type system with the subject reduction property. Finally, it is also shown that our typing rule properly extends the set of typeable processes.