{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,24]],"date-time":"2026-09-24T07:16:39Z","timestamp":1790234199755,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":46,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540421962","type":"print"},{"value":"9783540453321","type":"electronic"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"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":[[2001]]},"DOI":"10.1007\/3-540-45332-6_7","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T15:56:22Z","timestamp":1183478182000},"page":"177-206","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["Alias Types for Recursive Data Structures"],"prefix":"10.1007","author":[{"given":"David","family":"Walker","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Greg","family":"Morrisett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2001,6,13]]},"reference":[{"key":"7_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90181-R","volume":"111","author":"S. Abramsky","year":"1993","unstructured":"Samson Abramsky. Computational interpretations of linear logic. Theoretical Computer Science, 111:3\u201357, 1993.","journal-title":"Theoretical Computer Science"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Alexander Aiken, Manuel F\u00e4hndrich, and Raph Levien. Better static memory management: Improving region-based analysis of higher-order languages. In ACM Conference on Programming Language Design and Implementation, pages 174\u2013185, La Jolla, California, 1995.","DOI":"10.1145\/223428.207137"},{"key":"7_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-57529-4_42","volume-title":"Thirteenth Conference on the Foundations of Software Technology and Theoretical Computer Science","author":"E. Barendsen","year":"1993","unstructured":"Erik Barendsen and Sjaak Smetsers. Conventional and uniqueness typing in graph rewrite systems (extended abstract). In Thirteenth Conference on the Foundations of Software Technology and Theoretical Computer Science, pages 41\u201351, Bombay, 1993. In Shyamasundar, ed., Springer-Verlag, LNCS 761."},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"Michael Benedikt, Thomas Reps, and Mooly Sagiv. A decidable logic for describing linked data structures. In European Symposium on Programming, pages 2\u201319, Amsterdam, March 1999.","DOI":"10.1007\/3-540-49099-X_2"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Lars Birkedal, Mads Tofte, and Magnus Vejlstrup. From region inference to von Neumann machines via region representation inference. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 171\u2013183, St. Petersburg, January 1996.","DOI":"10.1145\/237721.237771"},{"key":"7_CR6","first-page":"23","volume-title":"Machine Intelligence","author":"R. M. Burstall","year":"1972","unstructured":"Rodney M. Burstall. Some techniques for proving correctness of programs which alter data structures. In Bernard Meltzer and Donald Michie, editors, Machine Intelligence, pages 23\u201350, Edinburgh, 1972. Edinburgh University Press."},{"key":"7_CR7","unstructured":"Perry Cheng and Chris Okasaki. Destination-passing style and generational garbage collection. Unpublished., November 1996."},{"issue":"2","key":"7_CR8","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1017\/S0956796800001660","volume":"6","author":"J. Chirimar","year":"1996","unstructured":"Jawahar Chirimar, Carl A. Gunter, and Jon G. Riecke. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming, 6(2):195\u2013244, March 1996. 202 D. Walker and G. Morrisett","journal-title":"Journal of Functional Programming"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Stephen Cook and Derek Oppen. An assertion language for data structures. In Second ACM Symposium on Principles of Programming Languages, pages 160\u2013166, New York, 1975. ACM Press.","DOI":"10.1145\/512976.512993"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 262\u2013275, San Antonio, January 1999.","DOI":"10.1145\/292540.292564"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Alain Deutsch. Interprocedural may-alias analysis for pointers: Beyond k-limiting. In ACM Conference on Programming Language Design and Implementation, pages 230\u2013241, Orlando, June 1994.","DOI":"10.1145\/773473.178263"},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Rakesh Ghiya and Laurie J. Hendren. Is it a tree, a DAG, or a cyclic graph? A shape analysis for heap-directed pointers in C. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 1\u201315, St. Petersburg Beach, Florida, January 1996.","DOI":"10.1145\/237721.237724"},{"key":"7_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Computer Science"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Dan Grossman and Greg Morrisett. Scalable certi cation for typed assembly language. In ACM SIGPLAN Workshop on Types in Compilation, Montreal, September 2000.","DOI":"10.1007\/3-540-45332-6_5"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Juan C. Guzm\u00e1n and Paul Hudak. Single-threaded polymorphic lambda calculus. In Symposium on Logic in Computer Science, pages 333\u2013343, Philadelphia, June 1990. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1990.113759"},{"issue":"4","key":"7_CR16","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1016\/0020-0190(94)90120-1","volume":"51","author":"R. Harper","year":"1994","unstructured":"Robert Harper. A simplified account of polymorphic references. Information Processing Letters, 51(4):201\u2013206, August 1994.","journal-title":"Information Processing Letters"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Samin Ishtiaq and Peter O\u2019Hearn. BI as an assertion language for mutable data structures. In Twenty-Eighth ACM Symposium on Principles of Programming Languages, pages 14\u201326, January 2001.","DOI":"10.1145\/373243.375719"},{"key":"7_CR18","unstructured":"Neil D. Jones and Steven Muchnick, editors. Flow analysis and optimization of Lisp-like structures. Prentice-Hall, 1981."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi. Quasi-linear types. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 29\u201342, San Antonio, January 1999.","DOI":"10.1145\/292540.292546"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","volume":"59","author":"Y. Lafont","year":"1988","unstructured":"Yves Lafont. The linear abstract machine. Theoretical Computer Science, 59:157\u2013180, 1988.","journal-title":"Theoretical Computer Science"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"James R. Larus and Paul N. Hil nger. Detecting conflicts between structure accesses. In ACM Conference on Programming Language Design and Implementation, pages 24\u201331, June 1988.","DOI":"10.1145\/960116.53993"},{"key":"7_CR22","unstructured":"James Richard Larus. Restructuring Symbolic Programs for Concurrent Execution on Multiprocessors. PhD thesis, University of California at Berkeley, May 1989. Available as Berkeley technical report UCB\/CSD 89\/502."},{"key":"7_CR23","series-title":"Lect Notes Comput Sci","volume-title":"ACM Conference on Functional Programming and Computer Architecture","author":"E. Meijer","year":"1991","unstructured":"Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes, and barbed wire. In ACM Conference on Functional Programming and Computer Architecture, volume 523 of Lecture Notes in Computer Science, Berlin, 1991. Springer-Verlag."},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Y. Minamide. A functional representation of data structures with a hole. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 75\u201384, San Diego, January 1998.","DOI":"10.1145\/268946.268953"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Y. Minamide, G. Morrisett, and R. Harper. Typed closure conversion. In Twenty-Third ACM Symposium on Principles of Programming Languages, pages 271\u2013283, St. Petersburg, January 1996.","DOI":"10.1145\/237721.237791"},{"key":"7_CR26","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0167-6423(93)90008-D","volume":"21","author":"B. M\u00f6ller","year":"1993","unstructured":"Bernhard M\u00f6ller. Towards pointer algebra. Science of Computer Programming, 21:57\u201390, 1993. Alias Types for Recursive Data Structures 203","journal-title":"Science of Computer Programming"},{"key":"7_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0055511","volume-title":"Second International Workshop on Types in Compilation","author":"G. Morrisett","year":"1998","unstructured":"Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based Typed Assembly Language. In Xavier Leroy and Atsushi Ohori, editors, Second International Workshop on Types in Compilation, volume 1473 of Lecture Notes in Computer Science, pages 28\u201352, Kyoto, March 1998. Springer-Verlag."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. In Twenty-Fifth ACM Symposium on Principles of Programming Languages, pages 85\u201397, San Diego, January 1998.","DOI":"10.21236\/ADA358572"},{"issue":"21","key":"7_CR29","first-page":"528","volume":"3","author":"G. Morrisett","year":"1999","unstructured":"Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language. ACM Transactions on Programming Languages and Systems, 3(21):528\u2013569, May 1999.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"George Necula and Peter Lee. The design and implementation of a certifying compiler. In ACM Conference on Programming Language Design and Implementation, pages 333\u2013344, Montreal, June 1998.","DOI":"10.1145\/277652.277752"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"John C. Reynolds. Syntactic control of interference. In Fifth ACM Symposium on Principles of Programming Languages, pages 39\u201346, Tucson, 1978.","DOI":"10.1145\/512760.512766"},{"key":"7_CR32","unstructured":"John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Millennial Perspectives in Computer Science, Palgrove, 2000."},{"issue":"1","key":"7_CR33","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/271510.271517","volume":"20","author":"M. Sagiv","year":"1998","unstructured":"Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1\u201350, January 1998.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"7_CR34","doi-asserted-by":"crossref","unstructured":"Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 105\u2013118, San Antonio, January 1999.","DOI":"10.1145\/292540.292552"},{"issue":"8","key":"7_CR35","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/363534.363554","volume":"10","author":"H. Schorr","year":"1967","unstructured":"H. Schorr and W. M. Waite. An efficient machine-independent procedure for garbage collection in various list structures. Communications of the ACM, 10(8):501\u2013506, August 1967.","journal-title":"Communications of the ACM"},{"key":"7_CR36","series-title":"Lect Notes Comput Sci","first-page":"366","volume-title":"European Symposium on Programming","author":"F. Smith","year":"2001","unstructured":"Frederick Smith, David Walker, and Greg Morrisett. Alias types. In European Symposium on Programming, volume 1782 of Lecture Notes in Computer Science, pages 366\u2013381, Berlin, March 2000. Springer-Verlag."},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Johnathan Sobel and Daniel Friedman. Recycling continuations. In ACM International Conference on Functional Programming, pages 251\u2013260, Baltimore, September 1998.","DOI":"10.1145\/291251.289452"},{"key":"7_CR38","unstructured":"TALx86. See http:\/\/www.cs.cornell.edu\/talc for an implementation of Typed Assembly Language based on Intel\u2019s IA32 architecture."},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Mads Tofte and Jean-Pierre Talpin. Implementation of the typed call-by-value \u03bb-calculus using a stack of regions. In Twenty-First ACM Symposium on Principles of Programming Languages, pages 188\u2013201, Portland, Oregon, January 1994.","DOI":"10.1145\/174675.177855"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"David N. Turner, Philip Wadler, and Christian Mossin. Once upon a type. In ACM International Conference on Functional Programming and Computer Architecture, San Diego, CA, June 1995.","DOI":"10.1145\/224164.224168"},{"key":"7_CR41","unstructured":"Philip Wadler. Listlessness is Better than Laziness. PhD thesis, Carnegie Mellon University, August 1985. Available as Carnegie Mellon University technical report CMU-CS-85-171."},{"key":"7_CR42","unstructured":"Philip Wadler. Linear types can change the world! In M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland. IFIP TC 2 Working Conference."},{"key":"7_CR43","unstructured":"David Walker. Typed Memory Management. PhD thesis, Cornell University, January 2001. To appear."},{"issue":"1","key":"7_CR44","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1006\/inco.1994.1093","volume":"115","author":"A. K. Wright","year":"1994","unstructured":"Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38\u201394, 1994. 204 D. Walker and G. Morrisett","journal-title":"Information and Computation"},{"key":"7_CR45","unstructured":"Hongwei Xi. Dependent Types in Practical Programming. PhD thesis, Carnegie Mellon University, 1999."},{"key":"7_CR46","unstructured":"Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In Twenty-Sixth ACM Symposium on Principles of Programming Languages, pages 214\u2013227, San Antonio, TX, January 1999."}],"container-title":["Lecture Notes in Computer Science","Types in Compilation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45332-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:02:25Z","timestamp":1737172945000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-45332-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540421962","9783540453321"],"references-count":46,"URL":"https:\/\/doi.org\/10.1007\/3-540-45332-6_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"13 June 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}