{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:27:21Z","timestamp":1767929241541,"version":"3.49.0"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":4634,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1996,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We develop an operational model for a language based on linear logic. Our semantics is \u2018low-level\u2019 enough to express sharing and copying while still being \u2018high-level\u2019 enough to abstract away from details of memory layout, and thus can be used to test potential applications of linear logic for analysis of programs. In particular, we demonstrate a precise relationship between type correctness for the linear-logic-based language and the correctness of a reference-counting interpretation of the primitives, and formulate and prove a result describing the possible run-time reference counts of values of linear type.<\/jats:p>","DOI":"10.1017\/s0956796800001660","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T16:11:13Z","timestamp":1226074273000},"page":"195-244","source":"Crossref","is-referenced-by-count":20,"title":["Reference counting as a computational interpretation of linear logic"],"prefix":"10.1017","volume":"6","author":[{"given":"Jawahar","family":"Chirimar","sequence":"first","affiliation":[]},{"given":"Carl A.","family":"Gunter","sequence":"additional","affiliation":[]},{"given":"Jon G.","family":"Riecke","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001660_ref028","volume-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"S0956796800001660_ref037","first-page":"151","volume-title":"Lisp and Functional Programming","author":"Wand","year":"1992"},{"key":"S0956796800001660_ref036","volume-title":"Workshop on Mathematical Foundations of Programming Language Semantics","author":"Wadler","year":"1993"},{"key":"S0956796800001660_ref034","volume-title":"Programming Concepts and Methods","author":"Wadler","year":"1990"},{"key":"S0956796800001660_ref033","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90095-B"},{"key":"S0956796800001660_ref020","first-page":"45","volume-title":"Abstract Interpretation of Declarative Languages","author":"Hudak","year":"1987"},{"key":"S0956796800001660_ref025","doi-asserted-by":"crossref","unstructured":"Lincoln P. and Mitchell J. C. (1992) Operational aspects of linear lambda calculus. Proceedings 7th Annual IEEE Symposium on Logic in Computer Science, pp. 235\u2013247.","DOI":"10.1109\/LICS.1992.185536"},{"key":"S0956796800001660_ref035","doi-asserted-by":"crossref","unstructured":"Wadler P. (1991) Is there a use for linear logic? Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, pp. 255\u2013273. ACM.","DOI":"10.1145\/115865.115894"},{"key":"S0956796800001660_ref007","article-title":"An optimizing compiler for a modern functional programming language","volume":"31","author":"Bloss","year":"1988","journal-title":"Computer Journal"},{"key":"S0956796800001660_ref030","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"S0956796800001660_ref010","doi-asserted-by":"publisher","DOI":"10.1145\/367487.367501"},{"key":"S0956796800001660_ref009","doi-asserted-by":"crossref","unstructured":"Chirimar J. , Gunter C. A. and Riecke J. G. (1992) Proving memory management invariants for a language based on linear logic. Proceedings of the ACM Conference on Lisp and Functional Programming, pp. 139\u2013150.","DOI":"10.1145\/141471.141527"},{"key":"S0956796800001660_ref002","volume-title":"Abstract Interpretation of Declarative Languages","author":"Abramsky","year":"1987"},{"key":"S0956796800001660_ref031","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90044-5"},{"key":"S0956796800001660_ref017","doi-asserted-by":"crossref","unstructured":"Guzm\u00e1n J. C. and Hudak P. (1990) Single-threaded polymorphic lambda calculus. Proceedings 5th Annual IEEE Symposium on Logic in Computer Science, pp. 333\u2013343.","DOI":"10.1109\/LICS.1990.113759"},{"key":"S0956796800001660_ref023","doi-asserted-by":"crossref","unstructured":"Launchbury J. (1993) A natural semantics for lazy evaluation. Conference Record of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 144\u2013154. ACM.","DOI":"10.1145\/158511.158618"},{"key":"S0956796800001660_ref013","doi-asserted-by":"crossref","unstructured":"Filinski A. (1992) Linear continuations. Conference Record of the 19th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 27\u201338. ACM.","DOI":"10.1145\/143165.143174"},{"key":"S0956796800001660_ref018","first-page":"13","volume-title":"Implementation of Lazy Functional Languages","author":"Holmstr\u00f6m","year":"1988"},{"key":"S0956796800001660_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037099"},{"key":"S0956796800001660_ref004","doi-asserted-by":"publisher","DOI":"10.1145\/359460.359470"},{"key":"S0956796800001660_ref027","volume-title":"Commentary on Standard ML","author":"Milner","year":"1991"},{"key":"S0956796800001660_ref003","volume-title":"Compiling with Continuations","author":"Appel","year":"1992"},{"key":"S0956796800001660_ref021","unstructured":"Kahn G. (1987) Natural semantics. Proceedings Symposium on Theoretical Aspects of Computer Science: Lecture Notes in Computer Science vol 247. Springer-Verlag."},{"key":"S0956796800001660_ref011","unstructured":"Despeyroux J. (1986) Proof of translation in natural semantics. Proceedings, Symposium on Logic in Computer Science. IEEE."},{"key":"S0956796800001660_ref022","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90100-4"},{"key":"S0956796800001660_ref029","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013458"},{"key":"S0956796800001660_ref014","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5298.001.0001","volume-title":"Performance and Evaluation of Lisp Systems","author":"Gabriel","year":"1985"},{"key":"S0956796800001660_ref026","unstructured":"Mackie I. (1991) Lilac: A functional programming language based on linear logic. Master's thesis, Imperial College, University of London."},{"key":"S0956796800001660_ref016","doi-asserted-by":"crossref","unstructured":"Goldberg B. and Gloger M. (1992) Polymorphic type reconstruction for garbage collection without tags. Proceedings of the ACM Conference on Lisp and Functional Programming, pp. 53\u201365. ACM.","DOI":"10.1145\/141478.141504"},{"key":"S0956796800001660_ref019","first-page":"479","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0956796800001660_ref024","doi-asserted-by":"crossref","unstructured":"Lawall J. L. and Danvy O. (1993) Separating stages in the continuation-passing style transformation. Conference Record of the 20th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 124\u2013136. ACM.","DOI":"10.1145\/158511.158613"},{"key":"S0956796800001660_ref001","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"S0956796800001660_ref008","doi-asserted-by":"crossref","unstructured":"Breazu-Tannen V. , Gunter C. and Scedrov A. (1990) Computing with coercions. Proceedings of the ACM Conference on Lisp and Functional Programming, pp. 44\u201360.","DOI":"10.1145\/91556.91590"},{"key":"S0956796800001660_ref032","volume-title":"An adequate operational semantics of sharing in lazy evaluation","author":"Purushothaman","year":"1991"},{"key":"S0956796800001660_ref015","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"S0956796800001660_ref038","unstructured":"Wise D. S. , Hess C. , Hunt W. and Ost E. (1992) Uniprocessor performance of reference-counting hardware heap. Unpublished manuscript."},{"key":"S0956796800001660_ref005","volume-title":"Term assignment for intuitionistic linear logic","author":"Benton","year":"1992"},{"key":"S0956796800001660_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/360336.360345"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001660","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T19:06:17Z","timestamp":1557774377000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001660\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,3]]},"references-count":38,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1996,3]]}},"alternative-id":["S0956796800001660"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001660","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,3]]}}}