{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,8,2]],"date-time":"2023-08-02T11:14:11Z","timestamp":1690974851300},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T00:00:00Z","timestamp":1226016000000},"content-version":"unspecified","delay-in-days":5059,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[1995,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We prove a strong normalisation result for the linear term calculus of Benton, Bierman, Hyland and de Paiva. Rather than prove the result from first principles, we give a translation of linear terms into terms in the second-order polymorphic lambda calculus (\u03bb2) which allows the result to be proved by appealing to the well-known strong normalisation property of \u03bb2. An interesting feature of the translation is that it makes use of the \u03bb2 coding of a coinductive datatype as the translation of the !-types (exponentials) of the linear calculus.<\/jats:p>","DOI":"10.1017\/s0956796800001246","type":"journal-article","created":{"date-parts":[[2008,11,7]],"date-time":"2008-11-07T16:12:13Z","timestamp":1226074333000},"page":"65-80","source":"Crossref","is-referenced-by-count":3,"title":["Strong normalisation for the linear term calculus"],"prefix":"10.1017","volume":"5","author":[{"given":"P. N.","family":"Benton","sequence":"first","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2008,11,7]]},"reference":[{"key":"S0956796800001246_ref001","doi-asserted-by":"crossref","unstructured":"Benton P. N. , Bierman G. M. , Hyland J. M. E. and de Paiva V. C. V. (1992) Term Assignment for Intuitionistic Linear Logic (Preliminary Report). Technical Report 262, Computer Laboratory, University of Cambridge.","DOI":"10.1007\/BFb0037099"},{"key":"S0956796800001246_ref005","article-title":"Reference Counting as a Computational Interpretation of Linear Logic","author":"Chirimar","year":"1995","journal-title":"Journal of Functional Programming"},{"key":"S0956796800001246_ref014","doi-asserted-by":"publisher","DOI":"10.2307\/2271658"},{"key":"S0956796800001246_ref002","first-page":"61","volume-title":"Selected Papers from Computer Science Logic 1992. LNCS 702","author":"Benton","year":"1992"},{"key":"S0956796800001246_ref004","unstructured":"Bierman G. M. (1993) On Intuitionistic Linear Logic. PhD thesis, Computer Laboratory, University of Cambridge."},{"key":"S0956796800001246_ref009","unstructured":"Hofmann M. and Pierce B. C. (1992) An Abstract View of Objects and Subtyping (Preliminary Report). Technical Report ECS-LFCS-92-226, Department of Computer Science, University of Edinburgh."},{"key":"S0956796800001246_ref003","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037099"},{"key":"S0956796800001246_ref006","first-page":"123","volume-title":"Logic and Computer Science","author":"Gallier","year":"1990"},{"key":"S0956796800001246_ref007","unstructured":"Girard J.-Y. (1972) Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur. Th\u00e8se de Doctorat d'Etat, Universit\u00e9 de Paris VII."},{"key":"S0956796800001246_ref008","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0956796800001246_ref010","volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0956796800001246_ref011","doi-asserted-by":"publisher","DOI":"10.1145\/44501.45065"},{"key":"S0956796800001246_ref013","volume-title":"Proc. Paris Colloquium on Programming. LNCS 19","author":"Reynolds","year":"1974"},{"key":"S0956796800001246_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0037118"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796800001246","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,14]],"date-time":"2019-05-14T20:10:13Z","timestamp":1557864613000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796800001246\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995,1]]},"references-count":14,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1995,1]]}},"alternative-id":["S0956796800001246"],"URL":"https:\/\/doi.org\/10.1017\/s0956796800001246","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995,1]]}}}