Objects and session types

被引:23
作者
Dezani-Ciancaglini, Mariangiola [1 ]
Drossopoulou, Sophia [2 ]
Mostrous, Dimitris [2 ]
Yoshida, Nobuko [2 ]
机构
[1] Univ Turin, Dipartimento Informat, IT-10149 Turin, Italy
[2] Univ London Imperial Coll Sci Technol & Med, Dept Comp, London SW7 2AZ, England
基金
英国工程与自然科学研究理事会;
关键词
ORIENTED LANGUAGES; PI-CALCULUS; PROGRESS; SYSTEM; !text type='JAVA']JAVA[!/text;
D O I
10.1016/j.ic.2008.03.028
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
A session takes place between two parties; after establishing a connection, each party interleaves local computations and communications (sending or receiving) with the other. Session types characterise such sessions in terms of the types of values communicated and the shape of protocols, and have been developed for the pi-calculus, CORBA interfaces, and functional languages. We study-the incorporation of session types into object-oriented languages through MOOSE, a multi-threaded language with session types, thread spawning, iterative, and higher-order sessions. Our design aims to consistently integrate the object-oriented programming style and sessions, and to be able to treat various case studies from the literature. We describe the design of MOOSE, its syntax, operational semantics, and type system, and develop a type inference system. After proving subject reduction, we establish the progress property: once a communication has been established, well-typed programs will never starve at communication points. (C) 2009 Elsevier Inc. All rights reserved.
引用
收藏
页码:595 / 641
页数:47
相关论文
共 53 条
[1]  
Acciai L, 2008, LECT NOTES COMPUT SC, V5065, P642, DOI 10.1007/978-3-540-68679-8_40
[2]  
AHERN A, 2005, OOPSLA 05, P403
[3]  
Bettini L, 2008, LECT NOTES COMPUT SC, V5065, P659, DOI 10.1007/978-3-540-68679-8_41
[4]  
Bierman G., 2003, 563 U CAMBR COMP LAB
[5]  
Bonelli E, 2005, J FUNCT PROGRAM, V15, P219, DOI 10.1017/S09567968O400543X
[6]  
BONELLI E, 2005, FGUC 04 ENTCS, V138, P3
[7]  
Bravetti M, 2007, LECT NOTES COMPUT SC, V4467, P96
[8]  
CAIRES L, 2006, LNCS, V4661, P98
[9]   Amalgamating sessions and methods in object-oriented languages with generics [J].
Capecchi, Sara ;
Coppo, Mario ;
Dezani-Ciancaglini, Mariangiola ;
Drossopoulou, Sophia ;
Giachino, Elena .
THEORETICAL COMPUTER SCIENCE, 2009, 410 (2-3) :142-167
[10]  
CARBONE M, 2007, DMC 06 ENTCS, V171, P127