{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,7]],"date-time":"2025-06-07T22:22:15Z","timestamp":1749334935528,"version":"3.40.3"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030644369"},{"type":"electronic","value":"9783030644376"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-64437-6_6","type":"book-chapter","created":{"date-parts":[[2020,11,26]],"date-time":"2020-11-26T13:02:45Z","timestamp":1606395765000},"page":"105-124","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Behavioural Types for Memory and Method Safety in a Core Object-Oriented Language"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5193-2914","authenticated-orcid":false,"given":"Mario","family":"Bravetti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[]},{"given":"Iaroslav","family":"Golovanov","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4603-5407","authenticated-orcid":false,"given":"Hans","family":"H\u00fcttel","sequence":"additional","affiliation":[]},{"given":"Mathias S.","family":"Jakobsen","sequence":"additional","affiliation":[]},{"given":"Mikkel K.","family":"Kettunen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8074-0380","authenticated-orcid":false,"given":"Ant\u00f3nio","family":"Ravara","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,24]]},"reference":[{"key":"6_CR1","unstructured":"https:\/\/github.com\/MungoTypesystem\/Mungo-Typechecker\/ExamplePrograms\/"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Aldrich, J.: The Plaid programming language (2010)","DOI":"10.1145\/2048147.2048197"},{"issue":"2\u20133","key":"6_CR3","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1561\/2500000031","volume":"3","author":"D Ancona","year":"2016","unstructured":"Ancona, D., et al.: Behavioral types in programming languages. Found. Trends Program. Lang. 3(2\u20133), 95\u2013230 (2016)","journal-title":"Found. Trends Program. Lang."},{"key":"6_CR4","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1016\/j.ic.2017.07.010","volume":"256","author":"M Bravetti","year":"2017","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: Undecidability of asynchronous session subtyping. Inf. Comput. 256, 300\u2013320 (2017)","journal-title":"Inf. Comput."},{"key":"6_CR5","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.tcs.2018.02.010","volume":"722","author":"M Bravetti","year":"2018","unstructured":"Bravetti, M., Carbone, M., Zavattaro, G.: On the boundary between decidability and undecidability of asynchronous session subtyping. Theoret. Comput. Sci. 722, 19\u201351 (2018)","journal-title":"Theoret. Comput. Sci."},{"key":"6_CR6","doi-asserted-by":"publisher","first-page":"100527","DOI":"10.1016\/j.jlamp.2020.100527","volume":"112","author":"M Bravetti","year":"2020","unstructured":"Bravetti, M., Zavattaro, G.: Process calculi as a tool for studying coordination, contracts and session types. J. Logical Algebraic Methods Program. 112, 100527 (2020)","journal-title":"J. Logical Algebraic Methods Program."},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Caires, L., Seco, J.C.: The type discipline of behavioral separation. In: The 40th Symposium on Principles of Programming Languages, POPL 2013, pp. 275\u2013286. ACM (2013)","DOI":"10.1145\/2480359.2429103"},{"issue":"3","key":"6_CR8","doi-asserted-by":"publisher","first-page":"197","DOI":"10.3233\/FI-2018-1663","volume":"159","author":"FS de Boer","year":"2018","unstructured":"de Boer, F.S., Bravetti, M., Lee, M.D., Zavattaro, G.: A petri net based modeling of active objects and futures. Fundamenta Informaticae 159(3), 197\u2013256 (2018)","journal-title":"Fundamenta Informaticae"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/978-3-540-24851-4_21","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"R DeLine","year":"2004","unstructured":"DeLine, R., F\u00e4hndrich, M.: Typestates for objects. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 465\u2013490. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_21"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.W.: Building and using pluggable type-checkers. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 681\u2013690. ACM (2011)","DOI":"10.1145\/1985793.1985889"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., DeLine, R.: Adoption and focus: practical linear types for imperative programming. In: Proceedings of PLDI 2002, pp. 13\u201324. ACM (2002)","DOI":"10.1145\/543552.512532"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Leino, K.R.M.: Declaring and checking non-null types in an object-oriented language. In: Proceedings of OOPSLA 2003, pp. 302\u2013312. ACM (2003)","DOI":"10.1145\/949343.949332"},{"key":"6_CR13","unstructured":"Franco, J., Tasos, A., Drossopoulou, S., Wrigstad, T., Eisenbach, S.: Safely abstracting memory layouts. CoRR, abs\/1901.08006 (2019)"},{"issue":"4","key":"6_CR14","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2629609","volume":"36","author":"R Garcia","year":"2014","unstructured":"Garcia, R., Tanter, \u00c9., Wolff, R., Aldrich, J.: Foundations of typestate-oriented programming. Trans. Program. Lang. Syst. 36(4), 1\u201344 (2014)","journal-title":"Trans. Program. Lang. Syst."},{"issue":"4","key":"6_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(4:12)2015","volume":"11","author":"SJ Gay","year":"2015","unstructured":"Gay, S.J., Gesbert, N., Ravara, A., Vasconcelos, V.T.: Modular session types for objects. Logical Methods Comput. Sci. 11(4), 1\u201376 (2015)","journal-title":"Logical Methods Comput. Sci."},{"issue":"2\u20133","key":"6_CR16","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"SJ Gay","year":"2005","unstructured":"Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Informatica 42(2\u20133), 191\u2013225 (2005)","journal-title":"Acta Informatica"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Grigore, R.: Java generics are turing complete. In: Proceedings of POPL 2017, pp. 73\u201385. ACM (2017)","DOI":"10.1145\/3093333.3009871"},{"key":"6_CR18","unstructured":"Hoare, T.: Null references: the billion dollar mistake (2009)"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/3-540-57208-2_35","volume-title":"CONCUR\u201993","author":"K Honda","year":"1993","unstructured":"Honda, K.: Types for dyadic interaction. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 509\u2013523. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57208-2_35"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-540-68863-1_9","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"L Hubert","year":"2008","unstructured":"Hubert, L., Jensen, T., Pichardie, D.: Semantic foundations and inference of non-null annotations. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 132\u2013149. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68863-1_9"},{"issue":"1","key":"6_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 1\u201336 (2016)","journal-title":"ACM Comput. Surv."},{"issue":"3","key":"6_CR22","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1145\/503502.503505","volume":"23","author":"A Igarashi","year":"2001","unstructured":"Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight java: a minimal core calculus for Java and GJ. Trans. Program. Lang. Syst. 23(3), 396\u2013450 (2001)","journal-title":"Trans. Program. Lang. Syst."},{"key":"6_CR23","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1016\/j.scico.2017.10.006","volume":"155","author":"D Kouzapas","year":"2018","unstructured":"Kouzapas, D., Dardha, O., Perera, R., Gay, S.J.: Typechecking protocols with Mungo and StMungo: a session type toolchain for Java. Sci. Comput. Program. 155, 52\u201375 (2018)","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"6_CR24","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1145\/3057284","volume":"60","author":"B Meyer","year":"2017","unstructured":"Meyer, B.: Ending null pointer crashes. Commun. ACM 60(5), 8\u20139 (2017)","journal-title":"Commun. ACM"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Milit\u00e3o, F., Aldrich, J., Caires, L.: Aliasing control with view-based typestate. In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, FTFJP 2010. ACM (2010)","DOI":"10.1145\/1924520.1924527"},{"key":"6_CR26","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R Milner","year":"1978","unstructured":"Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17, 348\u2013375 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Nierstrasz, O.: Regular types for active objects. In: Proceedings of the 8th Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA 1993), pp. 1\u201315. ACM (1993)","DOI":"10.1145\/165854.167976"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-540-73589-2_2","volume-title":"ECOOP 2007 \u2013 Object-Oriented Programming","author":"J Siek","year":"2007","unstructured":"Siek, J., Taha, W.: Gradual typing for objects. In: Ernst, E. (ed.) ECOOP 2007. LNCS, vol. 4609, pp. 2\u201327. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73589-2_2"},{"issue":"1","key":"6_CR29","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1109\/TSE.1986.6312929","volume":"12","author":"RE Strom","year":"1986","unstructured":"Strom, R.E., Yemini, S.: Typestate: a programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12(1), 157\u2013171 (1986)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"6_CR30","unstructured":"Sunshine, J.: Protocol programmability. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (2013). AAI3578659"},{"key":"6_CR31","doi-asserted-by":"crossref","unstructured":"Sunshine, J., Stork, S., Naden, K., Aldrich, J.: Changing state in the plaid language. In: Companion to OOPSLA 2011, pp. 37\u201338. ACM (2011)","DOI":"10.1145\/2048147.2048166"},{"key":"6_CR32","unstructured":"The Jedis Project: Jedis (2011\u20132019). https:\/\/github.com\/xetorthio\/jedis\/"},{"key":"6_CR33","unstructured":"The Redis Project: Redis (2011\u20132019). https:\/\/redis.io\/"},{"key":"6_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/978-3-030-50086-3_12","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"AL Voinea","year":"2020","unstructured":"Voinea, A.L., Dardha, O., Gay, S.J.: Typechecking Java protocols with [St]Mungo. In: Gotsman, A., Sokolova, A. (eds.) FORTE 2020. LNCS, vol. 12136, pp. 208\u2013224. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-50086-3_12"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-64437-6_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,24]],"date-time":"2021-04-24T01:49:27Z","timestamp":1619228967000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-64437-6_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030644369","9783030644376"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-64437-6_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"24 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Fukuoka","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Hotcrp.com","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"46","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"17","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"2","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"37% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}