{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:45Z","timestamp":1760202645357,"version":"3.41.2"},"reference-count":25,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,3,2]],"date-time":"2012-03-02T00:00:00Z","timestamp":1330646400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS. The calculus is equipped with a type system ensuring that well-typed processes are free from memory faults, memory leaks, and communication errors. The type system is essentially linear, but we show that linearity alone is inadequate, because it leaves room for scenarios where well-typed processes leak significant amounts of memory. We address these problems basing the type system upon an original variant of session types.<\/jats:p>","DOI":"10.2168\/lmcs-8(1:17)2012","type":"journal-article","created":{"date-parts":[[2012,9,6]],"date-time":"2012-09-06T10:03:11Z","timestamp":1346925791000},"source":"Crossref","is-referenced-by-count":15,"title":["Typing Copyless Message Passing"],"prefix":"10.46298","volume":"Volume 8, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2533-0511","authenticated-orcid":false,"given":"Viviana","family":"Bono","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9097-1297","authenticated-orcid":false,"given":"Luca","family":"Padovani","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,3,2]]},"reference":[{"key":"10.2168\/LMCS-8(1:17)2012_BCDDDY08","doi-asserted-by":"crossref","unstructured":"Lorenzo Bettini, Mario Coppo, Loris D'Antoni, Marco De Luca, Mariangiola Dezani-Ciancaglini, and Nobuko Yoshida. Global Progress in Dynamically Interleaved Multiparty Sessions. InProceedings of CONCUR'08, LNCS 5201, pages 418-433. Springer, 2008.","DOI":"10.1007\/978-3-540-85361-9_33"},{"key":"10.2168\/LMCS-8(1:17)2012_BonoMessaPadovani11","doi-asserted-by":"crossref","unstructured":"Viviana Bono, Chiara Messa, and Luca Padovani. Typing Copyless Message Passing. InProceedings of ESOP'11, LNCS 6602, pages 57-76. Springer, 2011.","DOI":"10.1007\/978-3-642-19718-5_4"},{"key":"10.2168\/LMCS-8(1:17)2012_BonoPadovani11","doi-asserted-by":"crossref","unstructured":"Viviana Bono and Luca Padovani. Polymorphic Endpoint Types for Copyless Message Passing. InProceedings of ICE'11, volume EPTCS 59, pages 52-67, 2011.","DOI":"10.4204\/EPTCS.59.5"},{"issue":"1\/2","key":"10.2168\/LMCS-8(1:17)2012_CardelliMartiniMitchellScedrov94","first-page":"4","volume":"109","author":"Luca Cardelli, Simone Martini, John C. M","year":"1994","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:17)2012_CastagnaDezaniGiachinoPadovani09","doi-asserted-by":"crossref","unstructured":"Giuseppe Castagna, Mariangiola Dezani-Ciancaglini, Elena Giachino, and Luca Padovani. Foundations of Session Types. InProceedings of PPDP'09, pages 219-230. ACM, 2009.","DOI":"10.1145\/1599410.1599437"},{"issue":"2","key":"10.2168\/LMCS-8(1:17)2012_ColazzoGhelli05","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1016\/j.ic.2004.11.003","volume":"198","author":"Dario Colazzo and Giorgio Ghelli","year":"2005","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-8(1:17)2012_Courcelle83","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(83)90059-2","volume":"25","author":"Bruno Courcelle","year":"1983","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-8(1:17)2012_Fahndrich06","doi-asserted-by":"crossref","unstructured":"Manuel F\u00e4hndrich, Mark Aiken, Chris Hawblitzel, Orion Hodson, Galen Hunt, James R. Larus, and Steven Levi. Language Support for Fast and Reliable Message-based Communication in Singularity OS. InProceedings of EuroSys'06, pages 177-190. ACM, 2006.","DOI":"10.1145\/1217935.1217953"},{"issue":"5","key":"10.2168\/LMCS-8(1:17)2012_Gay08","doi-asserted-by":"crossref","first-page":"895","DOI":"10.1017\/S0960129508006944","volume":"18","author":"Simon Gay","year":"2008","journal-title":"Mathematical Structures in Computer Science 2008"},{"issue":"2-3","key":"10.2168\/LMCS-8(1:17)2012_GayHole05","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/s00236-005-0177-z","volume":"42","author":"Simon Gay and Malcolm Hole","year":"2005","journal-title":"Acta Informatica"},{"issue":"01","key":"10.2168\/LMCS-8(1:17)2012_GayVasconcelos10","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1017\/S0956796809990268","volume":"20","author":"Simon Gay and Vasco T. Vasconcelos","year":"2010","journal-title":"Journal of Functional Programming"},{"key":"10.2168\/LMCS-8(1:17)2012_GiuntiVasconcelos10","doi-asserted-by":"crossref","unstructured":"Marco Giunti and Vasco Thudichum Vasconcelos. A Linear Account of Session Types in the Pi Calculus. InProceedings of CONCUR'10, volume LNCS 6269, pages 432-446, 2010.","DOI":"10.1007\/978-3-642-15375-4_30"},{"key":"10.2168\/LMCS-8(1:17)2012_Honda93","doi-asserted-by":"crossref","unstructured":"Kohei Honda. Types for Dyadic Interaction. InProceedings of CONCUR'93, LNCS 715, pages 509-523. Springer, 1993.","DOI":"10.1007\/3-540-57208-2_35"},{"key":"10.2168\/LMCS-8(1:17)2012_HondaVasconcelosKubo98","doi-asserted-by":"crossref","unstructured":"Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language Primitives and Type Disciplines for Structured Communication-based Programming. InProceedings of ESOP'98, LNCS 1381, pages 122-138. Springer, 1998.","DOI":"10.1007\/BFb0053567"},{"key":"10.2168\/LMCS-8(1:17)2012_SingularityOverview05","unstructured":"Galen Hunt, James Larus, Mart\u00edn Abadi, Mark Aiken, Paul Barham, Manuel F\u00e4hndrich, Chris Hawblitzel, Orion Hodson, Steven Levi, Nick Murphy, Bjarne Steensgaard, David Tarditi, Ted Wobber, and Brian Zill. An Overview of the Singularity Project. Technical Report MSR-TR-2005-135, Microsoft Research, 2005."},{"key":"10.2168\/LMCS-8(1:17)2012_HuntLarus2007","first-page":"37","volume":"41","author":"Galen C. Hunt and James R. Larus","year":"2007","journal-title":"SIGOPS Operating Systems Review"},{"key":"10.2168\/LMCS-8(1:17)2012_Jeffrey01","doi-asserted-by":"crossref","unstructured":"Alan Jeffrey. A Symbolic Labelled Transition System for Coinductive Subtyping ofFmu leqTypes. InProceedings of LICS'01, pages 323-333. IEEE, 2001.","DOI":"10.1109\/LICS.2001.932508"},{"key":"10.2168\/LMCS-8(1:17)2012_SDN5","unstructured":"Microsoft. Singularity Design Note 5: Channel Contracts. Technical report, Microsoft Research, 2004. Available at http:\/\/www.codeplex.com\/singularity."},{"key":"10.2168\/LMCS-8(1:17)2012_OHearnReynoldsYang01","doi-asserted-by":"crossref","unstructured":"Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. InProceedings of CSL'01, LNCS 2142, pages 1-19. Springer, 2001.","DOI":"10.1007\/3-540-44802-0_1"},{"key":"10.2168\/LMCS-8(1:17)2012_Padovani09","doi-asserted-by":"crossref","unstructured":"Luca Padovani. Session Types at the Mirror. InProceedings of ICE'09, volume EPTCS 12, pages 71-86, 2009.","DOI":"10.4204\/EPTCS.12.5"},{"key":"10.2168\/LMCS-8(1:17)2012_StengelBultan09","doi-asserted-by":"crossref","unstructured":"Zachary Stengel and Tevfik Bultan. Analyzing Singularity Channel Contracts. InProceedings of ISSTA'09, pages 13-24. ACM, 2009.","DOI":"10.1145\/1572272.1572275"},{"key":"10.2168\/LMCS-8(1:17)2012_Vasconcelos09","doi-asserted-by":"crossref","unstructured":"Vasco Thudichum Vasconcelos. Fundamentals of Session Types. InProceedings of SFM'09, volume LNCS 5569, pages 158-186. Springer, 2009.","DOI":"10.1007\/978-3-642-01918-0_4"},{"key":"10.2168\/LMCS-8(1:17)2012_Villard11","unstructured":"Jules Villard.Heaps and Hops. PhD thesis, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France, 2011."},{"key":"10.2168\/LMCS-8(1:17)2012_VillardLozesCalcagno09","doi-asserted-by":"crossref","unstructured":"Jules Villard, \u00c9tienne Lozes, and Cristiano Calcagno. Proving Copyless Message Passing. InProceedings of APLAS'09, LNCS 5904, pages 194-209. Springer, 2009.","DOI":"10.1007\/978-3-642-10672-9_15"},{"key":"10.2168\/LMCS-8(1:17)2012_VillardLozesCalcagno10","doi-asserted-by":"crossref","unstructured":"Jules Villard, \u00c9tienne Lozes, and Cristiano Calcagno. Tracking Heaps That Hop with Heap-Hop. InProceedings of TACAS'10, LNCS 6015, pages 275-279. Springer, 2010.","DOI":"10.1007\/978-3-642-12002-2_23"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/798\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/798\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T23:10:17Z","timestamp":1744067417000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,3,2]]},"references-count":25,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(1:17)2012","relation":{"references":[{"id-type":"doi","id":"10.1007\/978-3-642-15375-4_30","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"1202.2086","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1202.2086","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,3,2]]},"article-number":"798"}}