{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:57Z","timestamp":1776316917601,"version":"3.50.1"},"reference-count":33,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[1987,2,1]],"date-time":"1987-02-01T00:00:00Z","timestamp":539136000000},"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":9663,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[1987,2]]},"DOI":"10.1016\/0890-5401(87)90042-3","type":"journal-article","created":{"date-parts":[[2004,12,2]],"date-time":"2004-12-02T00:24:20Z","timestamp":1101947060000},"page":"85-116","source":"Crossref","is-referenced-by-count":51,"title":["Type theories, normal forms, and D\u221e-lambda-models"],"prefix":"10.1016","volume":"72","author":[{"given":"M.","family":"Coppo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Dezani-Ciancaglini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Zacchi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0890-5401(87)90042-3_BIB1","series-title":"To H. B. Curry, Essay in Combinatory Logic, Lambda Calculus and Formalism","first-page":"225","article-title":"Comparing some classes of lambda calculus models","author":"Barendregt","year":"1980"},{"key":"10.1016\/0890-5401(87)90042-3_BIB2","series-title":"Logic Colloquium '82","first-page":"209","article-title":"Lambda calculus and its models","author":"Barendregt","year":"1983"},{"key":"10.1016\/0890-5401(87)90042-3_BIB3","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":"J. Symbolic Logic"},{"key":"10.1016\/0890-5401(87)90042-3_BIB4","author":"Barendregt","year":"1984"},{"key":"10.1016\/0890-5401(87)90042-3_BIB5","series-title":"\u03bb-Calculus and computer science theory","year":"1975"},{"key":"10.1016\/0890-5401(87)90042-3_BIB6","series-title":"Lecture Notes in Computer Science","first-page":"96","article-title":"\u03bb-Terms as total or partial functions on normal forms","author":"Dezani-Ciancaglini","year":"1975"},{"key":"10.1016\/0890-5401(87)90042-3_BIB7","first-page":"333","article-title":"Combinatory logic as a semigroup (abstract)","volume":"43","author":"Church","year":"1937","journal-title":"Bull. Amer. Math. Soc."},{"key":"10.1016\/0890-5401(87)90042-3_BIB8","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/BF02011875","article-title":"A new type assignment for \u03bb-terms","volume":"19","author":"Coppo","year":"1979","journal-title":"Arch. Math. Logik Grundlag."},{"key":"10.1016\/0890-5401(87)90042-3_BIB9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/3-540-09510-1_11","article-title":"Functional characterization of some semantic equalities inside \u03bb-calculus","author":"Coppo","year":"1979"},{"key":"10.1016\/0890-5401(87)90042-3_BIB10","series-title":"To H. B. Curry, Essays on Combinatory Logic, Lambda Calculus and Formalism","first-page":"535","article-title":"Principal type schemes and \u03bb-calculus semantics","author":"Coppo","year":"1980"},{"key":"10.1016\/0890-5401(87)90042-3_BIB11","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1002\/malq.19810270205","article-title":"Functional characters of solvable terms","volume":"27","author":"Coppo","year":"1981","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"10.1016\/0890-5401(87)90042-3_BIB12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/3-540-12727-5_2","article-title":"Applicative information systems","author":"Coppo","year":"1983"},{"key":"10.1016\/0890-5401(87)90042-3_BIB13","series-title":"Logic Colloquium '82","first-page":"241","article-title":"Extended type structures and filter lambda models","author":"Coppo","year":"1983"},{"key":"10.1016\/0890-5401(87)90042-3_BIB14","article-title":"Applicative Information Systems and Recursive Domain Equations","author":"Coppo","year":"1984"},{"key":"10.1016\/0890-5401(87)90042-3_BIB15","volume":"Vol. 1","author":"Curry","year":"1958"},{"key":"10.1016\/0890-5401(87)90042-3_BIB16","first-page":"130","article-title":"Maximal monoids of normal forms","volume":"2","author":"Dezani-Ciancaglini","year":"1982","journal-title":"Fund. Inform."},{"key":"10.1016\/0890-5401(87)90042-3_BIB17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1007\/3-540-13346-1_14","article-title":"F-Semantics for intersection type discipline","author":"Dezani-Ciancaglini","year":"1984"},{"key":"10.1016\/0890-5401(87)90042-3_BIB18","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19800261902","article-title":"Lambda calculus models and extensionality","volume":"26","author":"Hindley","year":"1980","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"10.1016\/0890-5401(87)90042-3_BIB19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/3-540-11494-7_15","article-title":"The simple semantics for Coppo-Dezani-Sall\u00e9 type assignment","author":"Hindley","year":"1982"},{"issue":"No. 1","key":"10.1016\/0890-5401(87)90042-3_BIB20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(83)90136-6","article-title":"The completeness theorem for typing \u03bb-terms","volume":"22","author":"Hindley","year":"1983","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(87)90042-3_BIB21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/BFb0029520","article-title":"A survey of some useful partial order relations on terms of the lambda calculus","author":"Hyland","year":"1975"},{"key":"10.1016\/0890-5401(87)90042-3_BIB22","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1112\/jlms\/s2-12.3.361","article-title":"A syntactic characterization of the equality in some models of the \u03bb-calculus","volume":"12","author":"Hyland","year":"1976","journal-title":"J. London Math. Soc."},{"key":"10.1016\/0890-5401(87)90042-3_BIB23","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","article-title":"What is a model of the \u03bb-calculus?","volume":"52","author":"Meyer","year":"1982","journal-title":"Inform. Contr."},{"key":"10.1016\/0890-5401(87)90042-3_BIB24","article-title":"Lambda Calculus Models of Programming Languages","author":"Morris","year":"1968"},{"key":"10.1016\/0890-5401(87)90042-3_BIB25","series-title":"A Set-Theoretical Definition of Application","author":"Plotkin","year":"1972"},{"key":"10.1016\/0890-5401(87)90042-3_BIB26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1007\/3-540-08860-1_30","article-title":"Une Extension de la Th\u00e9orie des Types","author":"Sall\u00e9","year":"1978"},{"key":"10.1016\/0890-5401(87)90042-3_BIB27","series-title":"Lecture Notes in Math.","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/BFb0073967","article-title":"Continuous lattices","author":"Scott","year":"1972"},{"key":"10.1016\/0890-5401(87)90042-3_BIB28","doi-asserted-by":"crossref","first-page":"522","DOI":"10.1137\/0205037","article-title":"Data types as lattices","volume":"5","author":"Scott","year":"1976","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0890-5401(87)90042-3_BIB29","author":"Scott","year":"1981"},{"key":"10.1016\/0890-5401(87)90042-3_BIB30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"577","DOI":"10.1007\/BFb0012801","article-title":"Domains for Denotational Semantics","author":"Scott","year":"1982"},{"key":"10.1016\/0890-5401(87)90042-3_BIB31","author":"Stenlund","year":"1972"},{"key":"10.1016\/0890-5401(87)90042-3_BIB32","doi-asserted-by":"crossref","first-page":"198","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0890-5401(87)90042-3_BIB33","doi-asserted-by":"crossref","first-page":"488","DOI":"10.1137\/0205036","article-title":"The Relation between Computational and Denotational Properties for D\u221e-models of the Lambda-Calculus","volume":"5","author":"Wadsworth","year":"1976","journal-title":"SIAM J. Comput."}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540187900423?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540187900423?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T18:29:05Z","timestamp":1549045745000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0890540187900423"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1987,2]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1987,2]]}},"alternative-id":["0890540187900423"],"URL":"https:\/\/doi.org\/10.1016\/0890-5401(87)90042-3","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[1987,2]]}}}