{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:55:59Z","timestamp":1776891359882,"version":"3.51.2"},"reference-count":36,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"2","license":[{"start":{"date-parts":[[2008,3,1]],"date-time":"2008-03-01T00:00:00Z","timestamp":1204329600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,3]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a \u201cread-only\u201d context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three\n                    <jats:italic>usage aspects<\/jats:italic>\n                    apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Kone\u010dn'y (In\n                    <jats:italic>TYPES 2002 workshop, Nijmegen, Proceedings<\/jats:italic>\n                    , Springer-Verlag, 2003).\n                  <\/jats:p>","DOI":"10.1017\/s0956796807006399","type":"journal-article","created":{"date-parts":[[2007,7,5]],"date-time":"2007-07-05T09:09:20Z","timestamp":1183626560000},"page":"141-178","source":"Crossref","is-referenced-by-count":7,"title":["A type system with usage aspects"],"prefix":"10.46298","volume":"18","author":[{"given":"DAVID","family":"ASPINALL","sequence":"first","affiliation":[]},{"given":"MARTIN","family":"HOFMANN","sequence":"additional","affiliation":[]},{"given":"MICHAL","family":"KONE\u010cN\u00dd","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,3,1]]},"reference":[{"key":"S0956796807006399_manual_ref-17","unstructured":"Kobayashi, N. (1998). Quasi-linear Types. Tech. rept. 98\u201302. Department of Information Science, University of Tokyo."},{"key":"S0956796807006399_manual_ref-34","doi-asserted-by":"publisher","DOI":"10.1109\/ICCL.1998.674169"},{"key":"S0956796807006399_manual_ref-21","doi-asserted-by":"crossref","unstructured":"MacKenzie, K. & Wolverson, N. (2004). Camelot and grail: resource-aware functional programming on the JVM. Trends in Functional Programing, Vol. 4. Bristol: Intellect, pp. 29\u201346.","DOI":"10.2307\/j.ctv36xvxxx.6"},{"key":"S0956796807006399_manual_ref-7","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44898-5_4"},{"key":"S0956796807006399_manual_ref-5","unstructured":"Aspinall, D. & Konevcn\u00fd, M. (2003, February). Type Systems for Resource Bounded Programming and Compilation Project Homepage. http:\/\/homepages.inf.ed.ac.uk\/da\/resbnd. Accessed 1 June 2007."},{"key":"S0956796807006399_manual_ref-8","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"S0956796807006399_manual_ref-1","unstructured":"Wikipedia article on the administrative normal form. (2007). http:\\\\en.wikipedia.org wiki\/Administrative_Normal_Form. Accessed March 27, 2007."},{"key":"S0956796807006399_manual_ref-14","first-page":"258","article-title":"A type system for bounded space and functional in-place update","volume":"7","author":"Hofmann","year":"2000","journal-title":"Nordic J. Comput."},{"key":"S0956796807006399_manual_ref-13","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"S0956796807006399_manual_ref-22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_23"},{"key":"S0956796807006399_manual_ref-15","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"S0956796807006399_manual_ref-18","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292546"},{"key":"S0956796807006399_manual_ref-24","unstructured":"Peyton, J. S. & Wansbrough, K. (2000, September). Simple usage polymorphism. In Proc. 3rd ACM SIGPLAN Workshop on Types in Compilation (TIC 2000). Technical Report CMU\u2013CS\u201300\u2013161."},{"key":"S0956796807006399_manual_ref-36","unstructured":"Yang, H. , & Reddy, U. (1997). Imperative lambda calculus revisited. Electronic manuscript."},{"key":"S0956796807006399_manual_ref-27","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"S0956796807006399_manual_ref-29","first-page":"366","volume-title":"9th European Symposium on Programming (ESOP'00)","author":"Smith","year":"2000"},{"key":"S0956796807006399_manual_ref-32","unstructured":"Wadler, P. (1990). Linear types can change the world. IFIP TC 2 Working Conference on Programming Concepts and Methods, M. Broy & C. B., Jones (eds), Sea of Gallilee, Israel: North-Holland, pp. 561\u2013581."},{"key":"S0956796807006399_manual_ref-10","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90110-F"},{"key":"S0956796807006399_manual_ref-4","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45927-8_4"},{"key":"S0956796807006399_manual_ref-16","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"S0956796807006399_manual_ref-6","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500070109"},{"key":"S0956796807006399_manual_ref-3","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021014.79255.33"},{"key":"S0956796807006399_manual_ref-20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_11"},{"key":"S0956796807006399_manual_ref-31","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"S0956796807006399_manual_ref-35","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46423-9_1"},{"key":"S0956796807006399_manual_ref-25","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766"},{"key":"S0956796807006399_manual_ref-11","doi-asserted-by":"publisher","DOI":"10.1145\/231379.231389"},{"key":"S0956796807006399_manual_ref-19","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44904-3_14"},{"key":"S0956796807006399_manual_ref-23","doi-asserted-by":"crossref","unstructured":"O'Hearn, P. W. , Takeyama, M. , Power, A. J. , & Tennent, R. D. (1995). Syntactic control of interference revisited. In MFPS XI, Conference on Mathematical Foundations of Program Semantics. Electronic Notes in Theoretical Computer Science, vol. 1. Elsevier.","DOI":"10.1016\/S1571-0661(04)00026-X"},{"key":"S0956796807006399_manual_ref-30","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"S0956796807006399_manual_ref-2","doi-asserted-by":"publisher","DOI":"10.1145\/781131.781146"},{"key":"S0956796807006399_manual_ref-33","first-page":"177","volume-title":"TIC '00: Selected Papers from the Third International Workshop on Types in Compilation","author":"Walker","year":"2001"},{"key":"S0956796807006399_manual_ref-28","unstructured":"Shankar, N. (1999, November). Efficiently Executing PVS. Project report, Computer Science Laboratory, SRI International, Menlo Park, CA."},{"key":"S0956796807006399_manual_ref-9","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45099-3_7"},{"key":"S0956796807006399_manual_ref-26","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"S0956796807006399_manual_ref-12","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512532"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796807006399","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:09Z","timestamp":1776889149000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796807006399\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,3]]},"references-count":36,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2008,7]]}},"alternative-id":["S0956796807006399"],"URL":"https:\/\/doi.org\/10.1017\/s0956796807006399","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,3]]}}}