{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,29]],"date-time":"2026-05-29T15:44:59Z","timestamp":1780069499898,"version":"3.54.0"},"reference-count":66,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2023,8,30]],"date-time":"2023-08-30T00:00:00Z","timestamp":1693353600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T014628\/1"],"award-info":[{"award-number":["EP\/T014628\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,8,30]]},"abstract":"<jats:p>The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the  \nsuccess of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks.<\/jats:p>\n          <jats:p>Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de\u2019Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.<\/jats:p>","DOI":"10.1145\/3607832","type":"journal-article","created":{"date-parts":[[2023,8,31]],"date-time":"2023-08-31T17:40:31Z","timestamp":1693503631000},"page":"78-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Special Delivery: Programming with Mailbox Types"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5143-5475","authenticated-orcid":false,"given":"Simon","family":"Fowler","sequence":"first","affiliation":[{"name":"University of Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2448-5394","authenticated-orcid":false,"given":"Duncan Paul","family":"Attard","sequence":"additional","affiliation":[{"name":"University of Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-7075-0611","authenticated-orcid":false,"given":"Franciszek","family":"Sowul","sequence":"additional","affiliation":[{"name":"University of Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3033-9091","authenticated-orcid":false,"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[{"name":"University of Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0190-7010","authenticated-orcid":false,"given":"Phil","family":"Trinder","sequence":"additional","affiliation":[{"name":"University of Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,8,31]]},"reference":[{"key":"e_1_2_1_1_1","first-page":"397","article-title":"L^ 3","volume":"77","author":"Ahmed Amal","year":"2007","unstructured":"Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L^ 3: A Linear Language with Locations. Fundam. Informaticae, 77, 4 (2007), 397\u2013449.","journal-title":"A Linear Language with Locations. Fundam. Informaticae"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90059-2"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00223-5"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000031"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"Mehdi Bagherzadeh and Hridesh Rajan. 2017. Order types: static reasoning about message races in asynchronous message passing concurrency. In AGERE!@SPLASH. ACM 21\u201330. https:\/\/doi.org\/10.1145\/3141834.3141837 10.1145\/3141834.3141837","DOI":"10.1145\/3141834.3141837"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38771-5_12"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Avik Chaudhuri. 2009. A Concurrent ML library in Concurrent Haskell. In ICFP. ACM 269\u2013280. https:\/\/doi.org\/10.1145\/1596550.1596589 10.1145\/1596550.1596589","DOI":"10.1145\/1596550.1596589"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1140335.1140356"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498666"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3064849"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71316-6_22"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.15"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24725-8_15"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Sebastian Erdweg Oliver Bracevac Edlira Kuci Matthias Krebs and Mira Mezini. 2015. A co-contextual formulation of type rules and its application to incremental type checking. In OOPSLA. ACM 880\u2013897. https:\/\/doi.org\/10.1145\/2814270.2814277 10.1145\/2814270.2814277","DOI":"10.1145\/2814270.2814277"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237805"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.223.3"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8126809"},{"key":"e_1_2_1_21_1","volume-title":"Franciszek Sowul, Simon J. Gay, and Phil Trinder.","author":"Fowler Simon","year":"2023","unstructured":"Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. 2023. Special Delivery: Programming with Mailbox Types (Extended Version). arxiv:2306.12935."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-19(3:3)2023"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.11"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990268"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.291.3"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/2271032"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3239332.3242765"},{"key":"e_1_2_1_28_1","first-page":"1","article-title":"Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In ECOOP (LIPIcs, Vol. 194)","volume":"10","author":"Harvey Paul","year":"2021","unstructured":"Paul Harvey, Simon Fowler, Ornela Dardha, and Simon J. Gay. 2021. Multiparty Session Types for Safe Runtime Adaptation in an Actor Language. In ECOOP (LIPIcs, Vol. 194). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 10:1\u201310:30.","journal-title":"Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2637647.2637651"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0053567"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2827695"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782634"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21464-6_7"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70592-5_22"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","unstructured":"Shams Mahmood Imam and Vivek Sarkar. 2014. Savina - An Actor Benchmark Suite: Enabling Empirical Evaluation of Actor Libraries. In AGERE!@SPLASH. ACM 67\u201380. https:\/\/doi.org\/10.1145\/2687357.2687368 10.1145\/2687357.2687368","DOI":"10.1145\/2687357.2687368"},{"key":"e_1_2_1_38_1","unstructured":"Sa\u0161a Juri\u0107. 2019. Elixir in Action. Manning."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47846-3_19"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","unstructured":"Naoki Kobayashi. 1999. Quasi-Linear Types. In POPL. ACM 29\u201342. https:\/\/doi.org\/10.1145\/292540.292546 10.1145\/292540.292546","DOI":"10.1145\/292540.292546"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2017.18"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_23"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.275.6"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21464-6_7"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Rumyana Neykova and Nobuko Yoshida. 2017. Let it recover: multiparty protocol-induced recovery. In CC. ACM 98\u2013108. https:\/\/doi.org\/10.1145\/3033019.3033031 10.1145\/3033019.3033031","DOI":"10.1145\/3033019.3033031"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(1:17)2017"},{"key":"e_1_2_1_48_1","doi-asserted-by":"crossref","unstructured":"Leo Osvald Gr\u00e9gory M. Essertel Xilun Wu Lilliam I. Gonz\u00e1lez Alay\u00f3n and Tiark Rompf. 2016. Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect. In OOPSLA. ACM 234\u2013251.","DOI":"10.1145\/3022671.2984009"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_6"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.22152\/programming-journal.org"},{"key":"e_1_2_1_51_1","unstructured":"Luca Padovani. 2018. Mailbox Calculus Checker. https:\/\/boystrange.github.io\/mcc\/"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2018.06.001"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3229062"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055063"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434303"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Alceste Scalas Nobuko Yoshida and Elias Benussi. 2019. Verifying message-passing programs with dependent behavioural types. In PLDI. ACM 502\u2013516. https:\/\/doi.org\/10.1145\/3314221.3322484 10.1145\/3314221.3322484","DOI":"10.1145\/3314221.3322484"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","unstructured":"Gerard Tabone and Adrian Francalanza. 2021. Session types in Elixir. In AGERE!@SPLASH. ACM 12\u201323. https:\/\/doi.org\/10.1145\/3486601.3486708 10.1145\/3486601.3486708","DOI":"10.1145\/3486601.3486708"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.365.2"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58184-7_118"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_13"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3107937"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.05.002"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681400001X"},{"key":"e_1_2_1_66_1","unstructured":"Noam Zeilberger. 2015. Balanced polymorphism and linear lambda calculus. Talk at TYPES. http:\/\/noamz.org\/papers\/linprin.pdf"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607832","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3607832","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:05Z","timestamp":1750178225000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3607832"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,30]]},"references-count":66,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2023,8,30]]}},"alternative-id":["10.1145\/3607832"],"URL":"https:\/\/doi.org\/10.1145\/3607832","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,30]]},"assertion":[{"value":"2023-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}