{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,30]],"date-time":"2026-09-30T15:21:03Z","timestamp":1790781663479,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540255932","type":"print"},{"value":"9783540320142","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11417170_22","type":"book-chapter","created":{"date-parts":[[2010,12,16]],"date-time":"2010-12-16T19:29:35Z","timestamp":1292527775000},"page":"293-307","source":"Crossref","is-referenced-by-count":33,"title":["L3: A Linear Language with Locations"],"prefix":"10.1007","author":[{"given":"Greg","family":"Morrisett","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amal","family":"Ahmed","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Fluet","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"DeLine, R., F\u00e4hndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI (2001)","DOI":"10.1145\/378795.378811"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., DeLine, R.: Adoption and focus: Practical linear types for imperative programming. In: PLDI (2002)","DOI":"10.1145\/512530.512532"},{"key":"22_CR3","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/319301.319345","volume":"21","author":"G. Morrisett","year":"1999","unstructured":"Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. TOPLAS\u00a021, 528\u2013569 (1999)","journal-title":"TOPLAS"},{"key":"22_CR4","first-page":"43","volume":"12","author":"G. Morrisett","year":"2002","unstructured":"Morrisett, G., Crary, K., Glew, N., Walker, D.: Stack-based typed assembly language. JFP\u00a012, 43\u201388 (2002)","journal-title":"JFP"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Aiken, A., Foster, J.S., Kodumal, J., Terauchi, T.: Checking and inferring local non-aliasing. In: PLDI (2003)","DOI":"10.1145\/781131.781146"},{"key":"22_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/3-540-46425-5_24","volume-title":"Programming Languages and Systems","author":"F. Smith","year":"2000","unstructured":"Smith, F., Walker, D.W., Morrisett, G.: Alias types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, p. 366. Springer, Heidelberg (2000)"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S., O\u2019Hearn, P.: BI as an assertion language for mutable data structures. In: POPL (2001)","DOI":"10.1145\/360204.375719"},{"key":"22_CR8","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: L3: A linear language with locations. Technical Report TR-24-04, Harvard University (2004)"},{"key":"22_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.Y. Girard","year":"1987","unstructured":"Girard, J.Y.: Linear logic. Theoretical Computer Science\u00a050, 1\u2013102 (1987)","journal-title":"Theoretical Computer Science"},{"key":"22_CR10","unstructured":"Wadler, P.: Linear types can change the world! In: Programming Concepts and Methods (1990)"},{"key":"22_CR11","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1145\/331605.331611","volume":"47","author":"P.W. O\u2019Hearn","year":"2000","unstructured":"O\u2019Hearn, P.W., Reynolds, J.C.: From Algol to polymorphic linear lambda-calculus. Journal of the ACM\u00a047, 167\u2013223 (2000)","journal-title":"Journal of the ACM"},{"key":"22_CR12","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/606666.606670","volume":"34","author":"R. Plasmeijer","year":"1999","unstructured":"Plasmeijer, R., van Eekelen, M.: Keep it clean: a unique approach to functional programming. ACM SIGPLAN Notices\u00a034, 23\u201331 (1999)","journal-title":"ACM SIGPLAN Notices"},{"key":"22_CR13","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1145\/142137.142162","volume":"27","author":"H. Baker","year":"1992","unstructured":"Baker, H.: Lively linear LISP\u2014look ma, no garbage. ACM SIGPLAN Notices\u00a027, 89\u201398 (1992)","journal-title":"ACM SIGPLAN Notices"},{"key":"22_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1017\/S0956796800001246","volume":"5","author":"P.N. Benton","year":"1995","unstructured":"Benton, P.N.: Strong normalisation for the linear term calculus. JFP\u00a05, 65\u201380 (1995)","journal-title":"JFP"},{"key":"22_CR15","unstructured":"Ahmed, A., Appel, A.W., Virga, R.: An indexed model of impredicative polymorphism and mutable references (2003), Available at http:\/\/www.cs.princeton.edu\/~appel\/papers\/impred.pdf"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-46425-5_11","volume-title":"Programming Languages and Systems","author":"M. Hofmann","year":"2000","unstructured":"Hofmann, M.: A type system for bouned space and functional in-place update. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol.\u00a01782, p. 165. Springer, Heidelberg (2000)"},{"key":"22_CR17","unstructured":"Cheney, J., Morrisett, G.: A linearly typed assembly language. Technical Report 2003-1900, Cornell University (2003)"},{"key":"22_CR18","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1023\/B:JARS.0000021014.79255.33","volume":"31","author":"D. Aspinall","year":"2003","unstructured":"Aspinall, D., Compagnoni, A.: Heap bounded assembly language. Journal of Automated Reasoning\u00a031, 261\u2013302 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"22_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45337-7_2","volume-title":"ECOOP 2001 - Object-Oriented Programming","author":"J. Boyland","year":"2001","unstructured":"Boyland, J., Noble, J., Retert, W.: Capabilities for aliasing: A generalization of uniqueness and read-only. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol.\u00a02072, p. 2. Springer, Heidelberg (2001)"},{"key":"22_CR20","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1145\/363911.363923","volume":"24","author":"D. Walker","year":"2000","unstructured":"Walker, D., Crary, K., Morrisett, G.: Typed memory management in a calculus of capabilities. TOPLAS\u00a024, 701\u2013771 (2000)","journal-title":"TOPLAS"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"Boyapati, C., S\u0103lcianu, A., Beebee, W., Rinard, M.: Ownership types for safe region-based memory management in real-time Java. In: PLDI (2003)","DOI":"10.1145\/781131.781168"},{"key":"22_CR22","series-title":"Lecture Notes in Computer Science","volume-title":"ECOOP 2003 - Object-Oriented Programming","author":"D. Clarke","year":"2003","unstructured":"Clarke, D., Wrigstad, T.: External uniqueness is unique enough. In: Cardelli, L. (ed.) ECOOP 2003. LNCS, vol.\u00a02743, Springer, Heidelberg (2003)"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Hicks, M., Morrisett, G., Grossman, D., Jim, T.: Experience with safe manual memory-management in Cyclone. In: ISMM (2004)","DOI":"10.1145\/1029873.1029883"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Grothoff, C., Palsberg, J., Vitek, J.: Encapsulating objects with confined types. In: OOPSLA (2001)","DOI":"10.1145\/504282.504300"},{"key":"22_CR25","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1002\/spe.369","volume":"31","author":"J. Vitek","year":"2001","unstructured":"Vitek, J., Bokowski, B.: Confined types in Java. Software \u2013 Practice and Experience\u00a031, 507\u2013532 (2001)","journal-title":"Software \u2013 Practice and Experience"},{"key":"22_CR26","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Lam, P., Rinard, M.: Role analysis. In: POPL (2002)","DOI":"10.1145\/503272.503276"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Igarashi, A., Kobayashi, N.: A generic type system for the Pi-calculus. In: POPL (2001)","DOI":"10.1145\/360204.360215"},{"key":"22_CR28","series-title":"Lecture Notes in Computer Science","volume-title":"PARLE \u201994 Parallel Architectures and Languages Europe","author":"K. Takeuchi","year":"1994","unstructured":"Takeuchi, K., Honda, K., Kubo, M.: An interaction-based language and its typing system. In: Halatsis, C., Philokyprou, G., Maritsas, D., Theodoridis, S. (eds.) PARLE 1994. LNCS, vol.\u00a0817, Springer, Heidelberg (1994)"},{"key":"22_CR29","doi-asserted-by":"publisher","first-page":"914","DOI":"10.1145\/330249.330251","volume":"21","author":"N. Kobayashi","year":"1999","unstructured":"Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the Pi-Calculus. TOPLAS\u00a021, 914\u2013947 (1999)","journal-title":"TOPLAS"}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11417170_22.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:51:55Z","timestamp":1605642715000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11417170_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540255932","9783540320142"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11417170_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}