{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:41:58Z","timestamp":1750459318024,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540433637"},{"type":"electronic","value":"9783540459279"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45927-8_4","type":"book-chapter","created":{"date-parts":[[2007,10,19]],"date-time":"2007-10-19T09:39:04Z","timestamp":1192786744000},"page":"36-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Another Type System for In-Place Update"],"prefix":"10.1007","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Hofmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"4_CR1","unstructured":"David Aspinall and Adriana Compagnoni. Heap bounded assembly language. Technical report, Division of Informatics, University of Edinburgh, 2002."},{"key":"4_CR2","unstructured":"David Aspinall and Martin Hofmann. Heap bounded functional programming in Java. Implementation experiments, 2001."},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"579","DOI":"10.1017\/S0960129500070109","volume":"6","author":"E. Barendsen","year":"1996","unstructured":"E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579\u2013612, 1996.","journal-title":"Mathematical Structures in Computer Science"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Proceedings ACM Principles of Programming Languages, pages 262\u2013275, 1999.","DOI":"10.1145\/292540.292564"},{"issue":"2","key":"4_CR5","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0304-3975(93)90110-F","volume":"118","author":"M. Draghicescu","year":"1993","unstructured":"M. Draghicescu and S. Purushothaman. A uniform treatment of order of evaluation and aggregate update. Theoretical Computer Science, 118(2):231\u2013262, September 1993.","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. Linear types and non size-increasing polynomial time computation. In Logic in Computer Science (LICS), pages 464\u2013476. IEEE, Computer Society Press, 1999.","DOI":"10.1109\/LICS.1999.782641"},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","first-page":"258","volume-title":"Nordic Journal of Computing","author":"M. Hofmann","year":"2000","unstructured":"Martin Hofmann. A type system for bounded space and functional in-place update. Nordic Journal of Computing, 7(4):258\u2013289, 2000. An extended abstract has appeared in Programming Languages and Systems, G. Smolka, ed., Springer LNCS, 2000."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Martin Hofmann. The strength of non size-increasing computation. In Proceedings ACM Principles of Programming Languages, 2002.","DOI":"10.1145\/503272.503297"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Samin Ishtiaq and Peter W. O\u2019Hearn. BI as an assertion language for mutable data structures. In Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 14\u201326, New York, 2001. ACM.","DOI":"10.1145\/373243.375719"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Naoki Kobayashi. Quasi-linear types. In Proceedings ACM Principles of Programming Languages, pages 29\u201342, 1999.","DOI":"10.1145\/292540.292546"},{"key":"4_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-55253-7_23","volume-title":"Observers for linear types","author":"M. Odersky","year":"1992","unstructured":"Martin Odersky. Observers for linear types. In B. Krieg-Br\u00fcckner, editor, ESOP\u2019 92: 4th European Symposium on Programming, Rennes, France, Proceedings, pages 390\u2013407. Springer-Verlag, February 1992. Lecture Notes in Computer Science 582."},{"issue":"2","key":"4_CR12","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. W. O\u2019Hearn","year":"1999","unstructured":"Peter W. O\u2019Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2):215\u2013243, 1999.","journal-title":"Bulletin of Symbolic Logic"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"P. W. O\u2019Hearn, M. Takeyama, A. J. Power, and R. D. Tennent. Syntactic control of interference revisited. In MFPS XI, Conference on Mathematical Foundations of Program Semantics, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995.","DOI":"10.1016\/S1571-0661(04)00026-X"},{"key":"4_CR14","unstructured":"Simon Peyton-Jones and Keith Wansbrough. Simple usage polymorphism. In Proc. 3rd ACM SIGPLAN Workshop on Types in Compilation, Montreal, September 2000."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"J. C. Reynolds. Syntactic control of interference. In Proc. Fifth ACM Symp. on Princ. of Prog. Lang. (POPL), 1978.","DOI":"10.1145\/512760.512766"},{"key":"4_CR16","unstructured":"John C. Reynolds. Intuitionistic reasoning about shared mutable data structure. In Jim Davies, Bill Roscoe, and Jim Woodcock, editors, Millennial Perspectives in Computer Science, pages 303\u2013321, Houndsmill, Hampshire, 2000. Palgrave."},{"key":"4_CR17","unstructured":"Natarajan Shankar. Efficiently executing PVS. Technical report, Computer Science Laboratory, SRI International, 1999."},{"key":"4_CR18","series-title":"Lect Notes Comput Sci","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":"Frederick Smith, David Walker, and Greg Morrisett. Alias types. In G. Smolka, editor, Programming Languages and Systems, volume 1782, pages 366\u2013381. Springer LNCS, 2000."},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1996.2613","volume":"132","author":"M. Tofte","year":"1997","unstructured":"M. Tofte and J.-P. Talpin. Region-based memory management. Information and Computation, 132(2):109\u2013176, 1997.","journal-title":"Information and Computation"},{"key":"4_CR20","unstructured":"Philip Wadler. Linear types can change the world. In M. Broy and C. B. Jones, editors, IFIP TC 2 Working Conference on Programming Concepts and Methods, pages 561\u2013581, Sea of Gallilee, Israel, 1990. North-Holland."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Mitchell Wand and William D. Clinger. Set constraints for destructive array update optimization. In Proc. IEEE Conf. on Computer Languages\u2019 98, pages 184\u2013193, 1998.","DOI":"10.1109\/ICCL.1998.674169"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Reinhard Wilhelm, Mooly Sagiv, and Thomas Reps. Shape analysis. In Proceedings Compiler Construction, CC 2000, 2000.","DOI":"10.1007\/3-540-46423-9_1"},{"key":"4_CR23","unstructured":"H. Yang and U. Reddy. Imperative lambda calculus revisited, 1997."}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45927-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T19:14:06Z","timestamp":1737486846000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45927-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540433637","9783540459279"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45927-8_4","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"14 March 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}