{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:24:21Z","timestamp":1761611061285,"version":"3.30.1"},"reference-count":26,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"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":4184,"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":[[2002,2]]},"DOI":"10.1016\/s0304-3975(00)00356-x","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:13:06Z","timestamp":1027591986000},"page":"341-398","source":"Crossref","is-referenced-by-count":5,"title":["Completeness of type assignment systems with intersection, union, and type quantifiers"],"prefix":"10.1016","volume":"272","author":[{"given":"Hirofumi","family":"Yokouchi","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00356-X_BIB1","first-page":"64","article-title":"Strong conjunction and intersection types","volume":"vol. 520","author":"Alessi","year":"1991"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB2","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":"Inform. Comput."},{"year":"1984","series-title":"The Lambda Calculus: Its Syntax and Semantics","author":"Barendregt","key":"10.1016\/S0304-3975(00)00356-X_BIB3"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB4","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"},{"year":"1965","series-title":"The Foundations of Mathematics","author":"Beth","key":"10.1016\/S0304-3975(00)00356-X_BIB5"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB6","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1016\/0168-0072(94)90034-5","article-title":"Combining type disciplines","volume":"66","author":"Cardone","year":"1994","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB7","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\/S0304-3975(00)00356-X_BIB8","series-title":"Logic and Computer Science","first-page":"123","article-title":"On Girard's \u201ccandidats de reductibilit\u00e9\u201d","author":"Gallier","year":"1990"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB9","doi-asserted-by":"crossref","unstructured":"G. Gentzen, Untersuchungen \u00fcber das logische Schlie\u00dfen, I, II Math. Zeitschr. 39 (1934) 176\u2013210, 405\u2013431.","DOI":"10.1007\/BF01201353"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB10","unstructured":"J.Y. Girard, Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur, Ph.D. Thesis, University of Paris VII, 1972."},{"key":"10.1016\/S0304-3975(00)00356-X_BIB11","doi-asserted-by":"crossref","first-page":"81","DOI":"10.2307\/2266967","article-title":"Completeness in the theory of types","volume":"15","author":"Henkin","year":"1950","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB12","first-page":"212","article-title":"The simple semantics for Coppo-Dezani-Sall\u00e9 types","volume":"vol. 137","author":"Hindley","year":"1982"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB13","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\/S0304-3975(00)00356-X_BIB14","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/0304-3975(83)90141-X","article-title":"Curry's type-rules are complete with respect to the F-semantics too","volume":"22","author":"Hindley","year":"1983","journal-title":"Theoret. Comput. Sci."},{"year":"1986","series-title":"Introduction to Combinators and \u03bb-Calculus","author":"Hindley","key":"10.1016\/S0304-3975(00)00356-X_BIB15"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB16","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0304-3975(86)90109-X","article-title":"Typing and computational properties of lambda expressions","volume":"44","author":"Leivant","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00356-X_BIB17","first-page":"95","article-title":"An ideal model for recursive polymorphic types","volume":"71","author":"MacQueen","year":"1986","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(00)00356-X_BIB18","doi-asserted-by":"crossref","first-page":"211","DOI":"10.1016\/0890-5401(88)90009-0","article-title":"Polymorphic type inference and containment","volume":"76","author":"Mitchell","year":"1988","journal-title":"Inform. Comput."},{"key":"10.1016\/S0304-3975(00)00356-X_BIB19","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1016\/0168-0072(91)90067-V","article-title":"Kripke-style models for typed lambda calculus","volume":"51","author":"Mitchell","year":"1991","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB20","doi-asserted-by":"crossref","first-page":"452","DOI":"10.2307\/2270331","article-title":"Hauptsatz for higher order logic","volume":"33","author":"Prawitz","year":"1968","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB21","doi-asserted-by":"crossref","first-page":"399","DOI":"10.2969\/jmsj\/01940399","article-title":"A proof of cut-elimination theorem in simple type theory","volume":"19","author":"Takahashi","year":"1967","journal-title":"J. Math. Soc. Japan"},{"year":"1975","series-title":"Proof Theory","author":"Takeuti","key":"10.1016\/S0304-3975(00)00356-X_BIB22"},{"year":"1988","series-title":"Constructivism in Mathematics: An introduction, vol. I, II","author":"Troelstra","key":"10.1016\/S0304-3975(00)00356-X_BIB23"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB24","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/0304-3975(94)90080-9","article-title":"F-semantics for type assignment systems","volume":"129","author":"Yokouchi","year":"1994","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(00)00356-X_BIB25","doi-asserted-by":"crossref","unstructured":"H. Yokouchi, Completeness of type assignment systems with intersection, union, and type quantifiers (extended abstract), in: Proceedings, Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998, pp. 368\u2013379.","DOI":"10.1109\/LICS.1998.705672"},{"key":"10.1016\/S0304-3975(00)00356-X_BIB26","unstructured":"H. Yokouchi, R. Kashima, Sequent calculi for type assignment and their completeness, 1997, manuscript."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750000356X?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S030439750000356X?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2024,12,3]],"date-time":"2024-12-03T15:49:18Z","timestamp":1733240958000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S030439750000356X"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":26,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["S030439750000356X"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00356-x","relation":{},"ISSN":["0304-3975"],"issn-type":[{"type":"print","value":"0304-3975"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}