{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:26:35Z","timestamp":1767929195791,"version":"3.49.0"},"reference-count":47,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,10,1]],"date-time":"1991-10-01T00:00:00Z","timestamp":686275200000},"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":7960,"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":[[1991,10]]},"DOI":"10.1016\/0304-3975(90)90108-t","type":"journal-article","created":{"date-parts":[[2002,7,26]],"date-time":"2002-07-26T03:47:37Z","timestamp":1027655257000},"page":"107-136","source":"Crossref","is-referenced-by-count":34,"title":["Type checking with universes"],"prefix":"10.1016","volume":"89","author":[{"given":"Robert","family":"Harper","sequence":"first","affiliation":[]},{"given":"Robert","family":"Pollack","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0304-3975(90)90108-T_BIB1","article-title":"The Lambda Calculus: Its Syntax and Semantics","volume":"Vol. 103","author":"Barendregt","year":"1984"},{"key":"10.1016\/0304-3975(90)90108-T_BIB2","doi-asserted-by":"crossref","unstructured":"R. Burstall and B. Lampson, A kernel language for abstract data types and modules, in: Kahn [28] 1\u201350.","DOI":"10.1007\/3-540-13346-1_1"},{"key":"10.1016\/0304-3975(90)90108-T_BIB3","unstructured":"L. Cardelli, Phase distinctions in type theory, Unpublished manuscript."},{"key":"10.1016\/0304-3975(90)90108-T_BIB4","series-title":"A polymorphic \u03bb-calculus with Type:Type","author":"Cardelli","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB5","series-title":"Technical Report 77\u2013236","article-title":"An algorithm for checking PL\/CV arithmetical inferences","author":"Chan","year":"1977"},{"key":"10.1016\/0304-3975(90)90108-T_BIB6","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbol. Logic"},{"key":"10.1016\/0304-3975(90)90108-T_BIB7","series-title":"Technical Report RR 416","article-title":"Natural semantics on the computer","author":"Cl\u00e9ment","year":"1985"},{"key":"10.1016\/0304-3975(90)90108-T_BIB8","series-title":"Logics of Programs","article-title":"Report on the type theory (V3) of the programming logic PL\/CV3","volume":"Vol. 131","author":"Constable","year":"1982"},{"issue":"1","key":"10.1016\/0304-3975(90)90108-T_BIB9","first-page":"72","article-title":"The type theory of PL\/CV3","volume":"7","author":"Constable","year":"1984","journal-title":"ACM Trans. Programm. Languages Systems"},{"key":"10.1016\/0304-3975(90)90108-T_BIB10","series-title":"Implementing Mathematics with the NuPRL Proof Developing System","author":"Constable","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB11","article-title":"Une Th\u00e9orie des Constructions","volume":"VII","author":"Coquand","year":"1985"},{"key":"10.1016\/0304-3975(90)90108-T_BIB12","series-title":"Proc. Symp. on Logic in Computer Science","first-page":"227","article-title":"An analysis of Girard's paradox","author":"Coquand","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB13","series-title":"Projet Formel","article-title":"The calculus of constructions: documentation and user's guide","author":"Coquand","year":"1989"},{"key":"10.1016\/0304-3975(90)90108-T_BIB14","series-title":"EUROCAL '85: European Conf. on Computer Algebra","first-page":"151","article-title":"Constructions: A higher-order proof system for mechanizing mathematics","volume":"Vol. 203","author":"Coquand","year":"1985"},{"key":"10.1016\/0304-3975(90)90108-T_BIB15","series-title":"Proc. 9th ACM Symp. on Principles of Programming Languages","first-page":"207","article-title":"Principal type schemes for functional programs","author":"Damas","year":"1982"},{"key":"10.1016\/0304-3975(90)90108-T_BIB16","doi-asserted-by":"crossref","unstructured":"N.G. De Bruijn, A survey of the project AUTOMATH, in: Seldin and Hindley [45] 589\u2013606.","DOI":"10.1016\/S0049-237X(08)70203-9"},{"key":"10.1016\/0304-3975(90)90108-T_BIB17","series-title":"Proc. 3rd Symp. on Logic in Computer Science","first-page":"264","article-title":"A categorical semantics of constructions","author":"Erhard","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB18","series-title":"Proc. 3rd Symp. on Logic in Computer Science","first-page":"61","article-title":"Characterization of typings in polymorphic type discipline","author":"Giannini","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB19","series-title":"Proc. 2nd Symp. on Logic in Computer Science","first-page":"194","article-title":"A framework for defining logics","author":"Harper","year":"1987"},{"key":"10.1016\/0304-3975(90)90108-T_BIB20","series-title":"Technical Report CMU-CS-89-173","article-title":"A framework for defining logics","author":"Harper","year":"1989"},{"key":"10.1016\/0304-3975(90)90108-T_BIB21","series-title":"TAPSOFT '87","article-title":"A type discipline for program modules","volume":"Vol. 250","author":"Harper","year":"1987"},{"key":"10.1016\/0304-3975(90)90108-T_BIB22","article-title":"Higher-order modules and the phase distinction","author":"Harper","year":"1989","journal-title":"POPL '90"},{"key":"10.1016\/0304-3975(90)90108-T_BIB23","series-title":"Technical Report TR 86\u2013760","article-title":"Impredicative strong existential equivalent to Type: Type","author":"Hook","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB24","unstructured":"W.A. Howard, The formulas-as-types notion of construction, in: Seldin and Hindley [45] 479\u2013490."},{"key":"10.1016\/0304-3975(90)90108-T_BIB25","series-title":"Proc. 2nd Symp. on Logic in Computer Science","first-page":"205","article-title":"The computational behavior of Girard's paradox","author":"Howe","year":"1987"},{"key":"10.1016\/0304-3975(90)90108-T_BIB26","author":"Huet","year":"1987","journal-title":"Extending the calculus of constructions with Type: Type"},{"key":"10.1016\/0304-3975(90)90108-T_BIB27","series-title":"Proc. Boulder Conf. on Categories in Computer Science","article-title":"The theory of constructions: categorical semantics and topos-theoretic models","author":"Hyland","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB28","series-title":"Semantics of Data Types","volume":"Vol. 173","year":"1984"},{"key":"10.1016\/0304-3975(90)90108-T_BIB29","series-title":"Technical Report ECS-LFCS-88-57","article-title":"A higher-order calculus and theory abstraction","author":"Luo","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB30","series-title":"Technical Report ECS-LFCS-88-58","article-title":"CC\u221e\u2282 and its metatheory","author":"Luo","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB31","series-title":"Proc. 4th Symp. on Logic in Computer Science","article-title":"Ecc, an extended calculus of constructions","author":"Luo","year":"1989"},{"key":"10.1016\/0304-3975(90)90108-T_BIB32","series-title":"Technical Report LFCS-TN-27","article-title":"How to use lego: A preliminary user's manual","author":"Luo","year":"1989"},{"key":"10.1016\/0304-3975(90)90108-T_BIB33","series-title":"Proc. 13th ACM Symp. on Principles of Programming Languages","article-title":"Using dependent types to express modular structure","author":"MacQueen","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB34","unstructured":"P. Martin-L\u00f6f, A theory of types, Unpublished manuscript."},{"key":"10.1016\/0304-3975(90)90108-T_BIB35","series-title":"Logic Colloquium '73","first-page":"73","article-title":"An intuitionistic theory of types: predicative part","volume":"Vol. 80","author":"Martin-L\u00f6f","year":"1975"},{"key":"10.1016\/0304-3975(90)90108-T_BIB36","series-title":"Proc. 6th Internat. Cong. for Logic, Methodology, and Philosophy of Science","first-page":"153","article-title":"Constructive mathematics and computer programming","author":"Martin-L\u00f6f","year":"1982"},{"key":"10.1016\/0304-3975(90)90108-T_BIB37","article-title":"Intuitionistic Type Theory","volume":"Vol. 1","author":"Martin-L\u00f6f","year":"1984"},{"key":"10.1016\/0304-3975(90)90108-T_BIB38","series-title":"Proc. 13th ACM Symp. on Principles of Programming Languages","article-title":"\u2018Type\u2019 is not a type: Preliminary report","author":"Meyer","year":"1986"},{"key":"10.1016\/0304-3975(90)90108-T_BIB39","doi-asserted-by":"crossref","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","article-title":"A theory of type polymorphism in programming languages","volume":"17","author":"Milner","year":"1978","journal-title":"J. Comput. System Sci."},{"key":"10.1016\/0304-3975(90)90108-T_BIB40","series-title":"The Definition of Standard ML","author":"Milner","year":"1990"},{"key":"10.1016\/0304-3975(90)90108-T_BIB41","series-title":"Proc. 15th ACM Symp. on Principles of Programming Languages","article-title":"The essence of ML","author":"Mitchell","year":"1988"},{"key":"10.1016\/0304-3975(90)90108-T_BIB42","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell, Type inference and type containment, in: Kahn [28] 257\u2013278.","DOI":"10.1007\/3-540-13346-1_13"},{"key":"10.1016\/0304-3975(90)90108-T_BIB43","series-title":"Proc. 12th ACM Symp. on Principles of Programming Languages","article-title":"Abstract types have existential type","author":"Mitchell","year":"1985"},{"key":"10.1016\/0304-3975(90)90108-T_BIB44","doi-asserted-by":"crossref","first-page":"222","DOI":"10.2307\/2369948","article-title":"Mathematical logic as based on a theory of types","volume":"30","author":"Russell","year":"1908","journal-title":"Amer. J. Math."},{"key":"10.1016\/0304-3975(90)90108-T_BIB45","year":"1980"},{"key":"10.1016\/0304-3975(90)90108-T_BIB46","series-title":"Ph.D. Thesis","article-title":"The Language Theory of AUTOMATH","author":"Van Daalen","year":"1980"},{"key":"10.1016\/0304-3975(90)90108-T_BIB47","volume":"Vol. 1","author":"Whitehead","year":"1925"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090108T?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:030439759090108T?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,13]],"date-time":"2019-04-13T03:55:38Z","timestamp":1555127738000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/030439759090108T"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,10]]},"references-count":47,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,10]]}},"alternative-id":["030439759090108T"],"URL":"https:\/\/doi.org\/10.1016\/0304-3975(90)90108-t","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1991,10]]}}}