<XML><RECORDS><RECORD><REFERENCE_TYPE>3</REFERENCE_TYPE><REFNUM>9301</REFNUM><AUTHORS><AUTHOR>Gay,S.J.</AUTHOR><AUTHOR>Vasconcelos,V.T.</AUTHOR><AUTHOR>Ravara,A.</AUTHOR><AUTHOR>Gesbert,N.</AUTHOR><AUTHOR>Caldeira,A.Z.</AUTHOR></AUTHORS><YEAR>2010</YEAR><TITLE>Modular Session Types for Distributed Object-Oriented Programming</TITLE><PLACE_PUBLISHED>POPL'10, 37th ACM symposium on Principles of programming languages, Madrid</PLACE_PUBLISHED><PUBLISHER>ACM</PUBLISHER><PAGES>299-312</PAGES><ISBN>978-1-60558-479-9</ISBN><LABEL>Gay:2010:9301</LABEL><KEYWORDS><KEYWORD>Session types</KEYWORD></KEYWORDS<ABSTRACT>Session types allow communication protocols to be specified typetheoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e. partitioned into separately callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e. objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. We also describe a prototype implementation as an extension of Java.</ABSTRACT><NOTES>Full version of the paper (with proofs) available as Technical Report TR-2010-308, Department of Computing Science, University of Glasgow</NOTES><URL>http://dx.doi.org/10.1145/1706299.1706335</URL></RECORD></RECORDS></XML>