IEICE TRANSACTIONS on Information
A Session Type System with Subject Reduction
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E95-D No.8 pp.2053-2064
- Publication Date
- 2012/08/01
- Publicized
- Online ISSN
- 1745-1361
- DOI
- 10.1587/transinf.E95.D.2053
- Type of Manuscript
- PAPER
- Category
- Software System
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Keigo IMAI, Shoji YUEN, Kiyoshi AGUSA, "A Session Type System with Subject Reduction" in IEICE TRANSACTIONS on Information,
vol. E95-D, no. 8, pp. 2053-2064, August 2012, doi: 10.1587/transinf.E95.D.2053.
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E95.D.2053/_p
Copy
@ARTICLE{e95-d_8_2053,
author={Keigo IMAI, Shoji YUEN, Kiyoshi AGUSA, },
journal={IEICE TRANSACTIONS on Information},
title={A Session Type System with Subject Reduction},
year={2012},
volume={E95-D},
number={8},
pages={2053-2064},
abstract={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.},
keywords={},
doi={10.1587/transinf.E95.D.2053},
ISSN={1745-1361},
month={August},}
Copy
TY - JOUR
TI - A Session Type System with Subject Reduction
T2 - IEICE TRANSACTIONS on Information
SP - 2053
EP - 2064
AU - Keigo IMAI
AU - Shoji YUEN
AU - Kiyoshi AGUSA
PY - 2012
DO - 10.1587/transinf.E95.D.2053
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E95-D
IS - 8
JA - IEICE TRANSACTIONS on Information
Y1 - August 2012
AB - 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.
ER -
English
