{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:52:52Z","timestamp":1762458772982,"version":"3.41.0"},"reference-count":51,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2010,1,2]],"date-time":"2010-01-02T00:00:00Z","timestamp":1262390400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGPLAN Not."],"published-print":{"date-parts":[[2010,1,2]]},"abstract":"<jats:p>\n            Session types allow communication protocols to be specified type-theoretically 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\n            <jats:italic>modularized<\/jats:italic>\n            , 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.\n          <\/jats:p>","DOI":"10.1145\/1707801.1706335","type":"journal-article","created":{"date-parts":[[2010,1,19]],"date-time":"2010-01-19T20:14:58Z","timestamp":1263932098000},"page":"299-312","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Modular session types for distributed object-oriented programming"],"prefix":"10.1145","volume":"45","author":[{"given":"Simon J.","family":"Gay","sequence":"first","affiliation":[{"name":"University of Glasgow, Glasgow, United Kingdom"}]},{"given":"Vasco T.","family":"Vasconcelos","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisboa, Portugal"}]},{"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisboa, Portugal"}]},{"given":"Nils","family":"Gesbert","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, United Kingdom"}]},{"given":"Alexandre Z.","family":"Caldeira","sequence":"additional","affiliation":[{"name":"University of Lisbon, Lisboa, Portugal"}]}],"member":"320","published-online":{"date-parts":[[2010,1,17]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"32","article-title":"Controlling sharing of state in data types. ECOOP","volume":"1241","author":"Almeida P. S.","year":"1997","unstructured":"P. S. Almeida . Balloon types : Controlling sharing of state in data types. ECOOP , Springer LNCS , 1241 : 32 -- 59 , 1997 . P. S. Almeida. Balloon types: Controlling sharing of state in data types. ECOOP, Springer LNCS, 1241:32--59, 1997.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/199818.199860"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449783"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297050"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081741"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1370175.1370213"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03013-0_10"},{"key":"e_1_2_1_8_1","first-page":"240","article-title":"Multipoint session types for a distributed calculus. TGC","volume":"4912","author":"Bonelli E.","year":"2007","unstructured":"E. Bonelli and A. Compagnoni . Multipoint session types for a distributed calculus. TGC , Springer LNCS , 4912 : 240 -- 256 , 2007 . E. Bonelli and A. Compagnoni. Multipoint session types for a distributed calculus. TGC, Springer LNCS, 4912:240--256, 2007.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.04.030"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.016"},{"key":"e_1_2_1_11_1","first-page":"2","article-title":"Structured global programming for communication behaviour. ESOP","volume":"4421","author":"Carbone M.","year":"2007","unstructured":"M. Carbone , K. Honda , and N. Yoshida . Structured global programming for communication behaviour. ESOP , Springer LNCS , 4421 : 2 -- 17 , 2007 . M. Carbone, K. Honda, and N. Yoshida. Structured global programming for communication behaviour. ESOP, Springer LNCS, 4421:2--17, 2007.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/565816.503278"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/286942.286947"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-008-0079-y"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/381694.378811"},{"key":"e_1_2_1_17_1","first-page":"299","article-title":"A distributed object-oriented language with session types. TGC","volume":"3705","author":"Dezani-Ciancaglini M.","year":"2005","unstructured":"M. Dezani-Ciancaglini , N. Yoshida , A. Ahern , and S. Drossopolou . A distributed object-oriented language with session types. TGC , Springer LNCS , 3705 : 299 -- 318 , 2005 . M. Dezani-Ciancaglini, N. Yoshida, A. Ahern, and S. Drossopolou. A distributed object-oriented language with session types. TGC, Springer LNCS, 3705:299--318, 2005.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"e_1_2_1_19_1","first-page":"207","article-title":"Bounded session types for object-oriented languages. FMCO","volume":"4709","author":"Dezani-Ciancaglini M.","year":"2007","unstructured":"M. Dezani-Ciancaglini , S. Drossopoulou , E. Giachino , and N. Yoshida . Bounded session types for object-oriented languages. FMCO , Springer LNCS , 4709 : 207 -- 245 , 2007 . M. Dezani-Ciancaglini, S. Drossopoulou, E. Giachino, and N. Yoshida. Bounded session types for object-oriented languages. FMCO, Springer LNCS, 4709:207--245, 2007.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512532"},{"key":"e_1_2_1_21_1","first-page":"465","article-title":"Typestates for objects. ESOP","volume":"3086","author":"F\u00e4hndrich M.","year":"2004","unstructured":"M. F\u00e4hndrich and R. DeLine . Typestates for objects. ESOP , Springer LNCS , 3086 : 465 -- 490 , 2004 . M. F\u00e4hndrich and R. DeLine. Typestates for objects. ESOP, Springer LNCS, 3086:465--490, 2004.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217935.1217953"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512531"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/543552.512563"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/118014.117975"},{"key":"e_1_2_1_29_1","first-page":"122","article-title":"Language primitives and type discipline for structured communication-based programming. ESOP","volume":"1381","author":"Honda K.","year":"1998","unstructured":"K. Honda , V. Vasconcelos , and M. Kubo . Language primitives and type discipline for structured communication-based programming. ESOP , Springer LNCS , 1381 : 122 -- 138 , 1998 . K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. ESOP, Springer LNCS, 1381:122--138, 1998.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328472"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1057387.1057390"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00325-6"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/1107673.1107675"},{"key":"e_1_2_1_35_1","volume-title":"Resource usage analysis for the \u03c0-calculus. Logical Methods in Comp. Sci., 2(3:4):1--42","author":"Kobayashi N.","year":"2006","unstructured":"N. Kobayashi , K. Suenaga , and L. Wischik . Resource usage analysis for the \u03c0-calculus. Logical Methods in Comp. Sci., 2(3:4):1--42 , 2006 . N. Kobayashi, K. Suenaga, and L. Wischik. Resource usage analysis for the \u03c0-calculus. Logical Methods in Comp. Sci., 2(3:4):1--42, 2006."},{"key":"e_1_2_1_36_1","unstructured":"L. G. Mezzina. Typing Services. PhD thesis IMT Institute for Advanced Studies Lucca Italy 2009.  L. G. Mezzina. Typing Services. PhD thesis IMT Institute for Advanced Studies Lucca Italy 2009."},{"key":"e_1_2_1_37_1","volume-title":"Design and implementation of a behaviorally typed programming system for web services. Master's thesis","author":"Milit\u00e3o F.","year":"2008","unstructured":"F. Milit\u00e3o . Design and implementation of a behaviorally typed programming system for web services. Master's thesis , New University of Lisbon , 2008 . F. Milit\u00e3o. Design and implementation of a behaviorally typed programming system for web services. Master's thesis, New University of Lisbon, 2008."},{"key":"e_1_2_1_38_1","volume-title":"A session object calculus for structured communication-based programming. Submitted","author":"Mostrous D.","year":"2008","unstructured":"D. Mostrous and N. Yoshida . A session object calculus for structured communication-based programming. Submitted , 2008 . D. Mostrous and N. Yoshida. A session object calculus for structured communication-based programming. Submitted, 2008."},{"key":"e_1_2_1_39_1","first-page":"56","article-title":"An implementation of session types. PADL","volume":"3057","author":"Neubauer M.","year":"2004","unstructured":"M. Neubauer and P. Thiemann . An implementation of session types. PADL , Springer LNCS , 3057 : 56 -- 70 , 2004 . M. Neubauer and P. Thiemann. An implementation of session types. PADL, Springer LNCS, 3057:56--70, 2004.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_40_1","first-page":"99","volume-title":"Object-Oriented Software Composition","author":"Nierstrasz O.","year":"1995","unstructured":"O. Nierstrasz . Regular types for active objects . In Object-Oriented Software Composition , pages 99 -- 121 . Prentice Hall , 1995 . O. Nierstrasz. Regular types for active objects. In Object-Oriented Software Composition, pages 99--121. Prentice Hall, 1995."},{"key":"e_1_2_1_41_1","first-page":"138","article-title":"Polyglot: an extensible compiler framework for Java. Compiler Construction","volume":"2622","author":"Nystrom N.","year":"2003","unstructured":"N. Nystrom , M. R. Clarkson , and A. C. Myers . Polyglot: an extensible compiler framework for Java. Compiler Construction , Springer LNCS , 2622 : 138 -- 152 , 2003 . N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: an extensible compiler framework for Java. Compiler Construction, Springer LNCS, 2622:138--152, 2003.","journal-title":"Springer LNCS"},{"key":"e_1_2_1_42_1","volume-title":"IWACO (ECOOP workshop)","author":"\u00d6stlund J.","year":"2007","unstructured":"J. \u00d6stlund , T. Wrigstad , D. Clarke , and B. \u00c5kerblom . Ownership, uniqueness and immutability . In IWACO (ECOOP workshop) , 2007 . J. \u00d6stlund, T. Wrigstad, D. Clarke, and B. \u00c5kerblom. Ownership, uniqueness and immutability. In IWACO (ECOOP workshop), 2007."},{"key":"e_1_2_1_43_1","volume-title":"MIT Press","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . MIT Press , 2002 . B. C. Pierce. Types and Programming Languages. MIT Press, 2002."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411290"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0096-0551(01)00019-4"},{"key":"e_1_2_1_46_1","first-page":"1","article-title":"Types for active objects with static deadlock prevention","volume":"49","author":"Puntigam F.","year":"2001","unstructured":"F. Puntigam and C. Peter . Types for active objects with static deadlock prevention . Fundamenta Informatic\u00e6 , 49 : 1 -- 27 , 2001 . F. Puntigam and C. Peter. Types for active objects with static deadlock prevention. Fundamenta Informatic\u00e6, 49:1--27, 2001.","journal-title":"Fundamenta Informatic\u00e6"},{"key":"e_1_2_1_47_1","volume-title":"Typing non-uniform concurrent objects. CONCUR","author":"Ravara A.","year":"1877","unstructured":"A. Ravara and V. T. Vasconcelos . Typing non-uniform concurrent objects. CONCUR , Springer LNCS , 1877 : 474--488, 2000. A. Ravara and V. T. Vasconcelos. Typing non-uniform concurrent objects. CONCUR, Springer LNCS, 1877:474--488, 2000."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1986.6312929"},{"key":"e_1_2_1_49_1","first-page":"398","article-title":"An interaction-based language and its typing system. PARLE","volume":"817","author":"Takeuchi K.","year":"1994","unstructured":"K. Takeuchi , K. Honda , and M. Kubo . An interaction-based language and its typing system. PARLE , Springer LNCS , 817 : 398 -- 413 , 1994 . K. Takeuchi, K. Honda, and M. Kubo. An interaction-based language and its typing system. PARLE, Springer LNCS, 817:398--413, 1994.","journal-title":"Springer LNCS"},{"issue":"4","key":"e_1_2_1_50_1","first-page":"583","article-title":"Typing the behavior of software components using session types","volume":"73","author":"Vallecillo A.","year":"2006","unstructured":"A. Vallecillo , V. T. Vasconcelos , and A. Ravara . Typing the behavior of software components using session types . Fundamenta Informatic\u00e6 , 73 ( 4 ): 583 -- 598 , 2006 . A. Vallecillo, V. T. Vasconcelos, and A. Ravara. Typing the behavior of software components using session types. Fundamenta Informatic\u00e6, 73(4):583--598, 2006.","journal-title":"Fundamenta Informatic\u00e6"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"e_1_2_1_52_1","volume-title":"FOOL","author":"Vasconcelos V. T.","year":"2009","unstructured":"V. T. Vasconcelos , S. J. Gay , A. Ravara , N. Gesbert , and A. Z. Caldeira . Dynamic interfaces . FOOL , 2009 . V. T. Vasconcelos, S. J. Gay, A. Ravara, N. Gesbert, and A. Z. Caldeira. Dynamic interfaces. FOOL, 2009."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["ACM SIGPLAN Notices"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1707801.1706335","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1707801.1706335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T12:45:36Z","timestamp":1750250736000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1707801.1706335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,1,2]]},"references-count":51,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2010,1,2]]}},"alternative-id":["10.1145\/1707801.1706335"],"URL":"https:\/\/doi.org\/10.1145\/1707801.1706335","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1706299.1706335","asserted-by":"subject"}]},"ISSN":["0362-1340","1558-1160"],"issn-type":[{"type":"print","value":"0362-1340"},{"type":"electronic","value":"1558-1160"}],"subject":[],"published":{"date-parts":[[2010,1,2]]},"assertion":[{"value":"2010-01-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}