{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T22:52:51Z","timestamp":1672613571616},"reference-count":23,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"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":3607,"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":[[2003,9]]},"DOI":"10.1016\/s0890-5401(03)00089-0","type":"journal-article","created":{"date-parts":[[2003,6,2]],"date-time":"2003-06-02T19:15:45Z","timestamp":1054581345000},"page":"211-232","source":"Crossref","is-referenced-by-count":1,"title":["A binary modal logic for the intersection types of lambda-calculus"],"prefix":"10.1016","volume":"185","author":[{"given":"Silvio","family":"Valentini","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Matteo","family":"Viale","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0890-5401(03)00089-0_BIB1","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1006\/inco.1995.1086","article-title":"Intersection and Union types: syntax and semantics","volume":"119","author":"Barbanera","year":"1995","journal-title":"Information and Computation"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB2","series-title":"A Course in Mathematical Logic","author":"Bell","year":"1977"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB3","series-title":"The Lambda Calculus, its Syntax and Semantics","author":"Barendregt","year":"1984"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB4","doi-asserted-by":"crossref","first-page":"931","DOI":"10.2307\/2273659","article-title":"A filter lambda-model and the completeness of lambda-calculus","volume":"48","author":"Barendregt","year":"1983","journal-title":"Journal of symbolic logic"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB5","doi-asserted-by":"crossref","first-page":"719","DOI":"10.1017\/S0960129599002923","article-title":"A general method to prove the normalization theorem for first and second order typed \u03bb-calculi","volume":"9","author":"Capretta","year":"1999","journal-title":"Mathematical Structures in Computer Science"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB6","volume":"vol. I","author":"Curry","year":"1958"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB7","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1305\/ndjfl\/1039724889","article-title":"The \u201cRelevance\u201d of Intersection and Union types","volume":"38","author":"Dezani","year":"1997","journal-title":"Notre Dame Journal of Formal Logic"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB8","unstructured":"A. Frisch, Types r\u00e9cursifs, combinaisons bool\u00e9ennes et fonctions surcharg\u00e9es: application au typage de XML, Memoire de D.E.A. Laboratoire d\u2019Informatique de l\u2019Ecole Normale Sup\u00e9rieure, 2001"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB9","series-title":"The Collected Works of Gerhard Gentzen","author":"Szabo","year":"1969"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB10","series-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB11","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/0304-3975(83)90074-9","article-title":"Coppo-Dezani types do not correspond to propositional logic","volume":"28","author":"Hindley","year":"1984","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB12","unstructured":"G. Hughes, M. Cresswell, An Introduction to Modal Logic, Methuen, 1972"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB13","series-title":"Introduction to Metamathematics","author":"Kleene","year":"1952"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB14","series-title":"Lambda-Calculus, Types and Models","author":"Krivine","year":"1993"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB15","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/BF00650498","article-title":"The semantics of entailment III","volume":"1","author":"Meyer","year":"1972","journal-title":"Journal of Philosophical Logic"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB16","unstructured":"R.K. Meyer, unpublished manuscript"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB17","series-title":"To Essay on Combinatory Logic, Lambda Calculus and Formalism","first-page":"561","article-title":"A type assignment for strongly normalizable \u03bb-terms","author":"Pottinger","year":"1980"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB18","series-title":"Proof theory","author":"Takeuti","year":"1975"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB19","first-page":"119","article-title":"Cut elimination in a modal sequent calculus for K","volume":"1-B","author":"Valentini","year":"1982","journal-title":"Boll. Un. Mat. It."},{"key":"10.1016\/S0890-5401(03)00089-0_BIB20","first-page":"207","article-title":"A note on a straightforward proof of normal form theorem for simply typed \u03bb-calculi","volume":"8-A","author":"Valentini","year":"1994","journal-title":"Boll. Un. Mat. It."},{"issue":"7","key":"10.1016\/S0890-5401(03)00089-0_BIB21","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/s001530000070","article-title":"An elementary proof of strong normalization for intersection types","volume":"40","author":"Valentini","year":"2001","journal-title":"Archive for Mathematical Logic"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB22","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1093\/logcom\/4.2.109","article-title":"Intersection types as logical formulae","volume":"4","author":"Venneri","year":"1994","journal-title":"Journal of Logic and Computation"},{"key":"10.1016\/S0890-5401(03)00089-0_BIB23","unstructured":"Viale M., I tipi intersezione per il \u03bb-calcolo e la logica modale, Tesi di laurea, Universit\u00e0 di Pisa, 2001"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000890?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000890?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,3,20]],"date-time":"2019-03-20T19:56:02Z","timestamp":1553111762000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540103000890"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":23,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S0890540103000890"],"URL":"https:\/\/doi.org\/10.1016\/s0890-5401(03)00089-0","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}