{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,20]],"date-time":"2025-06-20T22:41:55Z","timestamp":1750459315261,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540140313"},{"type":"electronic","value":"9783540391852"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-39185-1_11","type":"book-chapter","created":{"date-parts":[[2007,10,26]],"date-time":"2007-10-26T20:13:43Z","timestamp":1193429623000},"page":"182-199","source":"Crossref","is-referenced-by-count":3,"title":["Typing with Conditions and Guarantees for Functional In-place Update"],"prefix":"10.1007","author":[{"given":"Michal","family":"Kone\u010dn\u00fd","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"11_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-45927-8_4","volume-title":"Programming Languages and Systems, Proceedings of 11th European Symposium on Programming","author":"D. Aspinall","year":"2002","unstructured":"David Aspinall and Martin Hofmann. Another type system for in-place update. In D. Le M\u00e9tayer, editor, Programming Languages and Systems, Proceedings of 11th European Symposium on Programming, pages 36\u201352. Springer-Verlag, 2002. Lecture Notes in Computer Science 2305."},{"unstructured":"Robert Atkey. First year progress report and thesis proposal: Type systems with explicit sharing. Available from: http:\/\/www.dcs.ed.ac.uk\/home\/roba , August 2002.","key":"11_CR2"},{"unstructured":"Robert Atkey. LFPL with explicit sharing and destruction. An unpublished draft, June 2002.","key":"11_CR3"},{"doi-asserted-by":"crossref","unstructured":"Juan C. Guzm\u00e1n and Paul Hudak. Single-threaded polymorphic lambda calculus. In Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, pages 333\u2013343, 1990.","key":"11_CR4","DOI":"10.1109\/LICS.1990.113759"},{"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. Computer Society Press, 1999.","key":"11_CR5","DOI":"10.1109\/LICS.1999.782641"},{"issue":"4","key":"11_CR6","first-page":"258","volume":"7","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.","journal-title":"Nordic Journal of Computing"},{"doi-asserted-by":"crossref","unstructured":"Martin Hofmann. The strength of non size-increasing computation. In Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, 2002.","key":"11_CR7","DOI":"10.1145\/503272.503297"},{"doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Steffen Jost. Static prediction of heap space usage for firstorder functional programs. In 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL\u2019 03), January 2003.","key":"11_CR8","DOI":"10.1145\/604131.604148"},{"unstructured":"Steffen Jost. Static prediction of dynamic space usage of linear functional programs. Master\u2019s thesis, Technische Universit\u00e4t Darmstadt, Fachbereich Mathematik, 2002.","key":"11_CR9"},{"unstructured":"C. Kirkegaard, R. Atkey, M. Kone\u010dn\u00fd, D. Aspinall, and M. Hofmann. Prototype compilers with resource-bounded type systems. Available from: http:\/\/www.dcs.ed.ac.uk\/home\/resbnd\/prototypes\/ , 2000\u20132003.","key":"11_CR10"},{"unstructured":"Michal Kone\u010dn\u00fd. LFPL with types for deep sharing. Technical Report EDI-INFRR-157, LFCS, Division of Informatics, University of Edinburgh, October 2002.","key":"11_CR11"},{"unstructured":"Michal Kone\u010dn\u00fd. Typing with conditions and guarantees in LFPL. Technical Report EDI-INF-RR-0151, LFCS, Division of Informatics, University of Edinburgh, October 2002.","key":"11_CR12"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P. O\u2019Hearn","year":"1999","unstructured":"P. O\u2019Hearn and D. Pym. The logic of bunched implications. Bulletin of Symbolic Logic, 5(2): 215\u2013243, 1999.","journal-title":"Bulletin of Symbolic Logic"},{"key":"11_CR14","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1016\/S0304-3975(98)00359-4","volume":"228","author":"P. W. O\u2019Hearn","year":"1999","unstructured":"P. W. O\u2019Hearn, A. J. Power, M. Takeyama, and R. D. Tennent. Syntactic control of interference revisited. Theoretical Computer Science, 228:211\u2013252, 1999.","journal-title":"Theoretical Computer Science"},{"unstructured":"Peter W. O\u2019Hearn. On bunched typing. To Appear in the Journal of Functional Programming, 2002.","key":"11_CR15"},{"doi-asserted-by":"crossref","unstructured":"John C. Reynolds. Syntactic control of interference. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 39\u201346. ACM Press, 1978.","key":"11_CR16","DOI":"10.1145\/512760.512766"},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/BFb0035793","volume-title":"Automata, Languages and Programming, 16th International Colloquium","author":"J. C. Reynolds","year":"1989","unstructured":"John C. Reynolds. Syntactic control of interference, part 2. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, 16th International Colloquium, pages 704\u2013722. Springer-Verlag, 1989. Lecture Notes in Computer Science 372."},{"unstructured":"John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, 2002.","key":"11_CR18"},{"key":"11_CR19","series-title":"Lect Notes Comput Sci","first-page":"366","volume-title":"ESOP 2000","author":"D. Walker","year":"2000","unstructured":"David Walker and Greg Morrisett. Alias types. In ESOP 2000, pages 366\u2013381, 2000. Lecture Notes in Computer Science 1782."},{"key":"11_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/3-540-45332-6_7","volume-title":"Types in Compilation 2000","author":"D. Walker","year":"2001","unstructured":"David Walker and Greg Morrisett. Alias types for recursive data structures. In Types in Compilation 2000, pages 177\u2013206, 2001. Lecture Notes in Computer Science 2071."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-39185-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,21]],"date-time":"2025-01-21T23:08:39Z","timestamp":1737500919000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-39185-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540140313","9783540391852"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-39185-1_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}