{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:10:58Z","timestamp":1761610258636,"version":"build-2065373602"},"reference-count":15,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2003,2,1]],"date-time":"2003-02-01T00:00:00Z","timestamp":1044057600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3831,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,2]]},"DOI":"10.1016\/s1571-0661(04)80488-2","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T12:47:47Z","timestamp":1096462067000},"page":"19-36","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":1,"title":["Strongly Normalising Cut-Elimination with Strict Intersection Types"],"prefix":"10.1016","volume":"70","author":[{"given":"Steffen","family":"van Bakel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB1","article-title":"Normalisation, Approximation, and Semantics for Combinator Systems","author":"Fern\u00e1ndez Bakel","year":"2002","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB2","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/0304-3975(92)90297-S","article-title":"Complete restrictions of the Intersection Type Discipline","volume":"102","author":"Bakel","year":"1992","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB3","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1016\/0304-3975(95)00073-6","article-title":"Intersection Type Assignment Systems","volume":"151","author":"Bakel","year":"1995","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB4","unstructured":"S. Bakel and M. Fern\u00e1ndez. Approximation and Normalization Results for Typeable Term Rewriting Systems. In Gilles Dowek, Jan Heering, Karl Meinke, and Bernhard M\u00f6ller, editors, Proceedings of HOA '95. Second International Workshop on Higher Order Algebra, Logic and Term Rewriting, Paderborn, Germany. Selected Papers, volume 1074 of Lecture Notes in Computer Science, pages 17\u201336. Springer-Verlag, 1996."},{"year":"1984","series-title":"The Lambda Calculus: its Syntax and Semantics","author":"Barendregt","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB5"},{"issue":"4","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB6","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","article-title":"A filter lambda model and the completeness of type assignment","volume":"48","author":"Barendregt","year":"1983","journal-title":"Journal of Symbolic Logic"},{"issue":"4","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB7","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1305\/ndjfl\/1093883253","article-title":"An Extension of the Basic Functionality Theory for the \u03bb-Calculus","volume":"21","author":"Coppo","year":"1980","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB8","doi-asserted-by":"crossref","unstructured":"H.B. Curry. Functionality in Combinatory Logic. In Proc. Nat. Acad. Sci. U.S.A., volume 20, pages 584\u2013590, 1934.","DOI":"10.1073\/pnas.20.11.584"},{"volume":"volume 1","year":"1958","author":"Curry","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB9"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB10","series-title":"Cambridge Tracts in Theoretical Computer Science","article-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB11","series-title":"Etudes et Recherches en Informatique","article-title":"Lambda-Calcul \u2013 Types et Mod\u00e8les","author":"Krivine","year":"1990"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB12","unstructured":"C. Retor\u00e9. A note on intersection types. INRIA Rapport de recherche 2431, INRIA, France, 1994."},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB13","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1016\/0304-3975(83)90069-5","article-title":"Principal type schemes for an extended type theory","volume":"28","author":"Ronchi Della Rocca","year":"1984","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"10.1016\/S1571-0661(04)80488-2_NEWBIB14","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)80488-2_NEWBIB15","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The relation between computational and denotational properties for Scott's D\u221e-models of the lambda-calculus","volume":"5","author":"Wadsworth","year":"1976","journal-title":"SIAM J. Comput"}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804882?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104804882?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:06:04Z","timestamp":1761609964000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104804882"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,2]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2003,2]]}},"alternative-id":["S1571066104804882"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80488-2","relation":{},"ISSN":["1571-0661"],"issn-type":[{"type":"print","value":"1571-0661"}],"subject":[],"published":{"date-parts":[[2003,2]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Strongly Normalising Cut-Elimination with Strict Intersection Types","name":"articletitle","label":"Article Title"},{"value":"Electronic Notes in Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S1571-0661(04)80488-2","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2003 Published by Elsevier B.V.","name":"copyright","label":"Copyright"}]}}