{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:50:27Z","timestamp":1781938227193,"version":"3.54.5"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032283573","type":"print"},{"value":"9783032283580","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-28358-0_10","type":"book-chapter","created":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:01:40Z","timestamp":1781935300000},"page":"195-215","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Proof of\u00a0Delivery: Mechanized Mailbox Types"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-9476-5727","authenticated-orcid":false,"given":"Edgard","family":"Schiebelbein","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1654-6118","authenticated-orcid":false,"given":"Annette","family":"Bieniusa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5143-5475","authenticated-orcid":false,"given":"Simon","family":"Fowler","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,6,21]]},"reference":[{"issue":"1","key":"10_CR1","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/s10817-020-09553-0","volume":"65","author":"G Ambal","year":"2020","unstructured":"Ambal, G., Lenglet, S., Schmitt, A.: HO$$\\pi $$ in Coq. J. Autom. Reason. 65(1), 75\u2013124 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09553-0","journal-title":"J. Autom. Reason."},{"key":"10_CR2","unstructured":"Armstrong, J.: Making reliable distributed systems in the presence of software errors. Ph.D. thesis, Royal Institute of Technology, Stockholm, Sweden (2003). https:\/\/nbn-resolving.org\/urn:nbn:se:kth:diva-3658"},{"issue":"4","key":"10_CR3","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"JA Brzozowski","year":"1964","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964). https:\/\/doi.org\/10.1145\/321239.321249","journal-title":"J. ACM"},{"issue":"3","key":"10_CR4","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-011-9225-2","volume":"49","author":"A Chargu\u00e9raud","year":"2012","unstructured":"Chargu\u00e9raud, A.: The locally nameless representation. J. Autom. Reason. 49(3), 363\u2013408 (2012). https:\/\/doi.org\/10.1007\/s10817-011-9225-2","journal-title":"J. Autom. Reason."},{"issue":"5","key":"10_CR5","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"75","author":"NG de Bruijn","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proc.) 75(5), 381\u2013392 (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","journal-title":"Indagationes Mathematicae (Proc.)"},{"key":"10_CR6","doi-asserted-by":"publisher","unstructured":"de\u2019Liguoro, U., Padovani, L.: Mailbox Types for Unordered Interactions. LIPIcs, Vol. 109, ECOOP 2018 109, 15:1\u201315:28 (2018). https:\/\/doi.org\/10.4230\/LIPICS.ECOOP.2018.15","DOI":"10.4230\/LIPICS.ECOOP.2018.15"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-540-24725-8_15","volume-title":"Programming Languages and Systems","author":"R Ennals","year":"2004","unstructured":"Ennals, R., Sharp, R., Mycroft, A.: Linear Types for Packet Processing. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 204\u2013218. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24725-8_15"},{"key":"10_CR8","doi-asserted-by":"publisher","unstructured":"Fowler, S., Attard, D.P., Marshall, D., Gay, S.J., Trinder, P.: Special Delivery: Programming with Mailbox Types (Extended Version) (2025). https:\/\/doi.org\/10.48550\/arXiv.2306.12935","DOI":"10.48550\/arXiv.2306.12935"},{"key":"10_CR9","doi-asserted-by":"publisher","unstructured":"Fowler, S., Attard, D.P., Sowul, F., Gay, S.J., Trinder, P.: Special delivery: programming with mailbox types. Proc. ACM Program. Lang. 7(ICFP), 78\u2013107 (2023). https:\/\/doi.org\/10.1145\/3607832","DOI":"10.1145\/3607832"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Fowler, S., Attard, D.P., Sowul, F., Gay, S.J., Trinder, P.: Special Delivery: Programming with Mailbox Types (Extended Version) (Jun 2023). https:\/\/doi.org\/10.48550\/arXiv.2306.12935","DOI":"10.48550\/arXiv.2306.12935"},{"issue":"3","key":"10_CR11","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1017\/S0960129514000231","volume":"26","author":"M Goto","year":"2016","unstructured":"Goto, M., Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: An extensible approach to session polymorphism. Math. Struct. Comput. Sci. 26(3), 465\u2013509 (2016). https:\/\/doi.org\/10.1017\/S0960129514000231","journal-title":"Math. Struct. Comput. Sci."},{"key":"10_CR12","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":"10_CR13","doi-asserted-by":"publisher","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. J. ACM 63(1), 9:1\u20139:67 (2016). https:\/\/doi.org\/10.1145\/2827695","DOI":"10.1145\/2827695"},{"key":"10_CR14","doi-asserted-by":"publisher","unstructured":"Kobayashi, N.: Quasi-linear types. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 29\u201342. POPL \u201999, Association for Computing Machinery, New York, NY, USA (1999). https:\/\/doi.org\/10.1145\/292540.292546","DOI":"10.1145\/292540.292546"},{"issue":"7","key":"10_CR15","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009). https:\/\/doi.org\/10.1145\/1538788.1538814","journal-title":"Commun. ACM"},{"issue":"2","key":"10_CR16","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1016\/S0890-5401(03)00088-9","volume":"185","author":"P Levy","year":"2003","unstructured":"Levy, P., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. Inf. Comput. 185(2), 182\u2013210 (2003). https:\/\/doi.org\/10.1016\/S0890-5401(03)00088-9","journal-title":"Inf. Comput."},{"key":"10_CR17","volume-title":"Types and Programming Languages","author":"BC Pierce","year":"2002","unstructured":"Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge, Mass (2002)"},{"key":"10_CR18","unstructured":"Pottier, F., Orr, K.: Dblib (2021). https:\/\/github.com\/rocq-community\/dblib. commit: 25469872c0ba99b046f7e5b8608205eeea5ac077"},{"key":"10_CR19","unstructured":"Stark, K.: Mechanising Syntax with Binders in Coq, Ph.D. thesis. Saarbr\u00fccken, Germany (2019)"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Team, T.R.D.: The Rocq Prover. Zenodo (2025). https:\/\/doi.org\/10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Thiemann, P.: Intrinsically-Typed Mechanized Semantics for Session Types. In: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, pp. 1\u201315. PPDP \u201919, Association for Computing Machinery, New York, NY, USA (2019). https:\/\/doi.org\/10.1145\/3354166.3354184","DOI":"10.1145\/3354166.3354184"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Tirore, D., Bengtson, J., Carbone, M.: Multiparty asynchronous session types: a mechanised proof of subject reduction. In: Aldrich, J., Silva, A. (eds.) 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0333, pp. 31:1\u201331:30. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2025.31","DOI":"10.4230\/LIPIcs.ECOOP.2025.31"},{"key":"10_CR23","unstructured":"Wadler, P., Kokke, W., Siek, J.G.: Programming Language Foundations in Agda (2022). https:\/\/plfa.inf.ed.ac.uk\/22.08\/"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-030-78089-0_9","volume-title":"Formal Techniques for Distributed Objects, Components, and Systems","author":"U Zalakain","year":"2021","unstructured":"Zalakain, U., Dardha, O.: $$\\pi $$ with Leftovers: A Mechanisation in Agda. In: Peters, K., Willemse, T.A.C. (eds.) FORTE 2021. LNCS, vol. 12719, pp. 157\u2013174. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-78089-0_9"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-28358-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T06:01:43Z","timestamp":1781935303000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-28358-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032283573","9783032283580"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-28358-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"21 June 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"COORDINATION","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Coordination Models and Languages","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Urbino","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 June 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 June 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"coordination2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.discotec.org\/2026\/coordination","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}