{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:26:58Z","timestamp":1774837618416,"version":"3.50.1"},"reference-count":56,"publisher":"Cambridge University Press (CUP)","issue":"6","license":[{"start":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T00:00:00Z","timestamp":1368057600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2013,12]]},"abstract":"<jats:p>Guaranteeing that the parties of a network application respect a given protocol is a crucial issue.<jats:italic>Session types<\/jats:italic>offer a method for abstracting and validating structured communication sequences (sessions).<jats:italic>Object-oriented programming<\/jats:italic>is an established paradigm for large scale applications.<jats:italic>Union types<\/jats:italic>, which behave as the least common supertypes of a set of classes, allow the implementation of unrelated classes with similar interfaces without additional programming. We have previously developed an integration of the features above into a class-based core language for building network applications, and this successfully amalgamated sessions and methods so that data can be exchanged flexibly according to communication protocols (session types).<\/jats:p><jats:p>The first aim of the work reported in this paper is to provide a full proof of the type safety property for that core language by renewing syntax, typing and semantics. In this way, static typechecking guarantees that after a session has started, computation cannot get stuck on a communication deadlock.<\/jats:p><jats:p>The second aim is to define a constraint-based type system that reconstructs the appropriate session types of session declarations instead of assuming that session types are explicitly given by the programmer. Such an algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.<\/jats:p>","DOI":"10.1017\/s0960129512000886","type":"journal-article","created":{"date-parts":[[2013,5,9]],"date-time":"2013-05-09T11:11:13Z","timestamp":1368097873000},"page":"1163-1219","source":"Crossref","is-referenced-by-count":1,"title":["Deriving session and union types for objects"],"prefix":"10.1017","volume":"23","author":[{"given":"LORENZO","family":"BETTINI","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"SARA","family":"CAPECCHI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"MARIANGIOLA","family":"DEZANI-CIANCAGLINI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"ELENA","family":"GIACHINO","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BETTI","family":"VENNERI","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2013,5,9]]},"reference":[{"key":"S0960129512000886_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_16"},{"key":"S0960129512000886_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.016"},{"key":"S0960129512000886_ref5","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2009.26"},{"key":"S0960129512000886_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503505"},{"key":"S0960129512000886_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_4"},{"key":"S0960129512000886_ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"S0960129512000886_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68679-8_41"},{"key":"S0960129512000886_ref1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1086"},{"key":"S0960129512000886_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_12"},{"key":"S0960129512000886_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00945-7_7"},{"key":"S0960129512000886_ref15","doi-asserted-by":"crossref","unstructured":"Carbone M. , Honda K. and Yoshida N. (2008a) Multiparty Asynchronous Session Types. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL'08) 273\u2013284.","DOI":"10.1145\/1328897.1328472"},{"key":"S0960129512000886_ref50","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/1122674.1122684","article-title":"Conversation with Steve Ross-Talbot","volume":"4","author":"Sparkes","year":"2006","journal-title":"ACM Queue"},{"key":"S0960129512000886_ref10","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.64.2"},{"key":"S0960129512000886_ref40","first-page":"22","article-title":"Language Primitives and Type Disciplines for Structured Communication-based Programming","volume":"1381","author":"Honda","year":"1998","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129512000886_ref8","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680400543X"},{"key":"S0960129512000886_ref13","first-page":"338","article-title":"Global Escape in Multiparty Sessions","volume":"8","author":"Capecchi","year":"2010","journal-title":"LIPIcs"},{"key":"S0960129512000886_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68265-3_2"},{"key":"S0960129512000886_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_2"},{"key":"S0960129512000886_ref36","doi-asserted-by":"crossref","unstructured":"Gay S. J. , Vasconcelos V. T. , Ravara A. , Gesbert N. and Caldeira A. Z. (2010) Modular Session Types for Distributed Object-oriented Programming. In POPL \u201810: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages 299\u2013312.","DOI":"10.1145\/1706299.1706335"},{"key":"S0960129512000886_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45337-7_4"},{"key":"S0960129512000886_ref54","unstructured":"Web Services Choreography Working Group (2002) Web Services Choreography Description Language. (Available at http:\/\/www.w3.org\/2002\/ws\/chor\/.)"},{"key":"S0960129512000886_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85361-9_32"},{"key":"S0960129512000886_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-72952-5_1"},{"key":"S0960129512000886_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.049"},{"key":"S0960129512000886_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599437"},{"key":"S0960129512000886_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_24"},{"key":"S0960129512000886_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_17"},{"key":"S0960129512000886_ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78663-4_18"},{"key":"S0960129512000886_ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74792-5_10"},{"key":"S0960129512000886_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78663-4_17"},{"key":"S0960129512000886_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80382-2"},{"key":"S0960129512000886_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/11785477_20"},{"key":"S0960129512000886_ref28","unstructured":"Drossopoulou S. , Dezani-Ciancaglini M. and Coppo M. (2007) Amalgamating the Session Types and the Object Oriented Programming Paradigms. Presented at MPOOL'07."},{"key":"S0960129512000886_ref29","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich M. , Aiken M. , Hawblitzel C. , Hodson O. , Hunt G. C. , Larus J. R. and Levi S. (2006) Language Support for Fast and Reliable Message-based Communication in Singularity OS. In Proceedings of the 1st ACM SIGOPS\/EuroSys European Conference on Computer Systems 2006 (EuroSys2006) 177\u2013190.","DOI":"10.1145\/1217935.1217953"},{"key":"S0960129512000886_ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.056"},{"key":"S0960129512000886_ref37","unstructured":"Giachino E. (2009) Session Types: Semantic Foundations and Object-Oriented Applications, Ph.D. thesis, Universit\u00e0 degli Studi di Torino and Universit\u00e9 Paris 7."},{"key":"S0960129512000886_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/1391289.1391293"},{"key":"S0960129512000886_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45070-2_8"},{"key":"S0960129512000886_ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140344"},{"key":"S0960129512000886_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/11580850_16"},{"key":"S0960129512000886_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129508006944"},{"key":"S0960129512000886_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"S0960129512000886_ref49","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129512000886_ref51","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"S0960129512000886_ref34","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-005-0177-z"},{"key":"S0960129512000886_ref47","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_23"},{"key":"S0960129512000886_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2008.03.028"},{"key":"S0960129512000886_ref35","unstructured":"Gay S. , Vasconcelos V. T. and Ravara A. (2003) Session Types for Inter-Process Communication. TR 2003\u2013133, Department of Computing, University of Glasgow."},{"key":"S0960129512000886_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"S0960129512000886_ref39","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/978-3-642-00590-9_23","article-title":"Global Principal Typing in Partially Commutative Asynchronous Sessions","volume":"5502","author":"Honda","year":"2009","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129512000886_ref41","first-page":"160","article-title":"Web Services, Mobile Processes and Types","volume":"91","author":"Honda","year":"2007","journal-title":"EATCS Bulletin"},{"key":"S0960129512000886_ref42","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_16"},{"key":"S0960129512000886_ref44","doi-asserted-by":"publisher","DOI":"10.5381\/jot.2007.6.2.a3"},{"key":"S0960129512000886_ref46","doi-asserted-by":"publisher","DOI":"10.1145\/960112.28718"},{"key":"S0960129512000886_ref53","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.06.028"},{"key":"S0960129512000886_ref55","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_10"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129512000886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,13]],"date-time":"2019-07-13T15:55:23Z","timestamp":1563033323000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129512000886\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5,9]]},"references-count":56,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,12]]}},"alternative-id":["S0960129512000886"],"URL":"https:\/\/doi.org\/10.1017\/s0960129512000886","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,5,9]]}}}