{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T12:42:31Z","timestamp":1784119351071,"version":"3.55.0"},"reference-count":48,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1993,4,1]],"date-time":"1993-04-01T00:00:00Z","timestamp":733622400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":7412,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[1993,4]]},"DOI":"10.1016\/0304-3975(93)90181-r","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"3-57","source":"Crossref","is-referenced-by-count":230,"title":["Computational interpretations of linear logic"],"prefix":"10.1016","volume":"111","author":[{"given":"Samson","family":"Abramsky","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(93)90181-R_BIB1","series-title":"Tech. Report DOC 90\/20","article-title":"Computational interpretations of linear logic","author":"Abramsky","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB2","series-title":"Abstract Interpretation for Declarative Languages","year":"1987"},{"key":"10.1016\/0304-3975(93)90181-R_BIB3","series-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/0304-3975(93)90181-R_BIB4","doi-asserted-by":"crossref","unstructured":"H. Barendregt and K. Hemerik, Types in lambda calculi and programming languages, in: Proc. ESOP '90.","DOI":"10.1007\/3-540-52592-0_53"},{"key":"10.1016\/0304-3975(93)90181-R_BIB5","first-page":"81","article-title":"The chemical abstract machine","author":"Berry","year":"1990","journal-title":"Conf. Record of the 17th Ann. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(93)90181-R_BIB6","series-title":"Introduction to Functional Programming","author":"Bird","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB7","series-title":"Universal Algebra","author":"Cohn","year":"1981"},{"key":"10.1016\/0304-3975(93)90181-R_BIB8","first-page":"207","article-title":"Principal type schemes for functional programs","author":"Damas","year":"1982","journal-title":"Conf. Record of the 9th Ann. ACM Symp. on the Principles of Programming Languages"},{"key":"10.1016\/0304-3975(93)90181-R_BIB9","series-title":"Functional Programming","author":"Field","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB10","series-title":"Logic and Computer Science","article-title":"On Girard's \u201cCandidats de Reductibilit\u00e9\u201d","author":"Gallier","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB11","series-title":"Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"10.1016\/0304-3975(93)90181-R_BIB12","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","article-title":"Linear logic","volume":"50","author":"Girard","year":"1987","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(93)90181-R_BIB13","series-title":"Logic Colloquium '88","article-title":"Geometry of interaction 1: interpretation of system F","author":"Girard","year":"1989"},{"key":"10.1016\/0304-3975(93)90181-R_BIB14","first-page":"69","article-title":"Towards a geometry of interaction","volume":"Vol. 92","author":"Girard","year":"1989"},{"key":"10.1016\/0304-3975(93)90181-R_BIB15","volume":"Vol. 7","author":"Girard","year":"1989"},{"key":"10.1016\/0304-3975(93)90181-R_BIB16","series-title":"Proc. Math. Sci. Institute Workshop on Feasible Mathematics","article-title":"Bounded linear logic","author":"Girard","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB17","volume":"Vol. 217","year":"1986"},{"key":"10.1016\/0304-3975(93)90181-R_BIB18","series-title":"Functional Programming: Applications and Implementation","author":"Henderson","year":"1980"},{"key":"10.1016\/0304-3975(93)90181-R_BIB19","series-title":"Communicating Sequential Processes","author":"Hoare","year":"1985"},{"key":"10.1016\/0304-3975(93)90181-R_BIB20","series-title":"Proc. Workshop on Implementation of Lazy Functional Languages","first-page":"13","article-title":"Linear functional programming","author":"Holmstr\u00f6m","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB21","series-title":"Tech. Report YALEU\/DCS\/RR666","article-title":"Report on the functional programming language Haskell","author":"Hudak","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB22","series-title":"Logical Foundations of Functional Programming","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB23","series-title":"Proc. Workshop on Implementation of Lazy Functional Languages","author":"Karlsson","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB24","first-page":"22","article-title":"Natural semantics","volume":"Vol. 247","author":"Kahn","year":"1987"},{"key":"10.1016\/0304-3975(93)90181-R_BIB25","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1016\/0304-3975(88)90100-4","article-title":"The linear abstract machine","volume":"59","author":"Lafont","year":"1988","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(93)90181-R_BIB26","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","article-title":"The mechanical evaluation of expressions","volume":"6","author":"Landin","year":"1964","journal-title":"Comput. J."},{"key":"10.1016\/0304-3975(93)90181-R_BIB27_1","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/363744.363749","article-title":"A correspondence between ALGOL 60 and Church's lambda notation","volume":"8","author":"Landin","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(93)90181-R_BIB27_2","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1145\/363791.363804","article-title":"A correspondence between ALGOL 60 and Church's lambda notation","volume":"8","author":"Landin","year":"1965","journal-title":"Comm. ACM"},{"key":"10.1016\/0304-3975(93)90181-R_BIB28","series-title":"occam 2 Reference Manual","author":"INMOS LTD","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB29","volume":"Vol. 443","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/0304-3975(93)90181-R_BIB30","series-title":"Computer Programming and Formal Systems","first-page":"33","article-title":"A basis for a mathematical theory of computation","author":"McCarthy","year":"1963"},{"key":"10.1016\/0304-3975(93)90181-R_BIB31","series-title":"Proc. 3rd Ann. Symp. on Logic in Computer Science","first-page":"236","article-title":"Semantical paradigms","author":"Meyer","year":"1988"},{"key":"10.1016\/0304-3975(93)90181-R_BIB32","volume":"Vol. 92","author":"Milner","year":"1980"},{"key":"10.1016\/0304-3975(93)90181-R_BIB33","series-title":"Communication and Concurrency","author":"Milner","year":"1989"},{"key":"10.1016\/0304-3975(93)90181-R_BIB34","first-page":"167","article-title":"Functions as processes","volume":"Vol. 443","author":"Milner","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB35","series-title":"The Definitions of Standard ML","author":"Milner","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB36","first-page":"37","article-title":"Abstract types have existential type","author":"Mitchell","year":"1985","journal-title":"Conf. Record of the 12th Ann. ACM Symp. on Principles of Programming Languages"},{"key":"10.1016\/0304-3975(93)90181-R_BIB37","article-title":"The theory of practice of transforming call-by-need into call-by-value","volume":"Vol. 83","author":"Mycroft","year":"1980"},{"key":"10.1016\/0304-3975(93)90181-R_BIB38","series-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones","year":"1987"},{"key":"10.1016\/0304-3975(93)90181-R_BIB39","first-page":"125","article-title":"Call-by-name, call-by-value and the lambda calculus","volume":"1","author":"Plotkin","year":"1975","journal-title":"Comput. Sci."},{"key":"10.1016\/0304-3975(93)90181-R_BIB40","article-title":"Lectures on predomains and partial functions","author":"Plotkin","year":"1985","journal-title":"Notes for a course given at the Center for the Study of Language and Information, Stanford"},{"key":"10.1016\/0304-3975(93)90181-R_BIB41","first-page":"97","article-title":"Three approaches to type structure","volume":"Vol. 185","author":"Reynolds","year":"1985"},{"key":"10.1016\/0304-3975(93)90181-R_BIB42","article-title":"Complexity analysis for a lazy higher order language","author":"Sands","year":"1989","journal-title":"Proc. 2nd Glasgow Workshop on Functional Programming"},{"key":"10.1016\/0304-3975(93)90181-R_BIB43","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(89)90168-0","article-title":"A typed calculus based on a fragment of linear logic","volume":"68","author":"Solitro","year":"1989","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0304-3975(93)90181-R_BIB44","article-title":"Miranda - a non-strict functional language with polymorphic types","volume":"Vol. 201","author":"Turner","year":"1985"},{"key":"10.1016\/0304-3975(93)90181-R_BIB45","series-title":"Research Topics in Functional Programming","year":"1990"},{"key":"10.1016\/0304-3975(93)90181-R_BIB46","series-title":"Tech. Report 64\/89","article-title":"The judgement calculus for intuitionistic linear logic: proof theory and semantics","author":"Valentini","year":"1989"},{"key":"10.1016\/0304-3975(93)90181-R_BIB47","series-title":"Programming Concepts and Methods","article-title":"Linear types can change the world!","author":"Wadler","year":"1990"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759390181R?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759390181R?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T04:22:22Z","timestamp":1555129342000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759390181R"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,4]]},"references-count":48,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1993,4]]}},"alternative-id":["030439759390181R"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(93)90181-r","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1993,4]]}}}