{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,4,17]],"date-time":"2023-04-17T12:20:22Z","timestamp":1681734022602},"reference-count":71,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1991,1,1]],"date-time":"1991-01-01T00:00:00Z","timestamp":662688000000},"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":8233,"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":[[1991,1]]},"DOI":"10.1016\/0890-5401(91)90062-7","type":"journal-article","created":{"date-parts":[[2004,12,1]],"date-time":"2004-12-01T19:24:20Z","timestamp":1101929060000},"page":"107-137","source":"Crossref","is-referenced-by-count":17,"title":["A higher-order calculus and theory abstraction"],"prefix":"10.1016","volume":"90","author":[{"given":"Zhaohui","family":"Luo","sequence":"first","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/0890-5401(91)90062-7_BIB1","series-title":"talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi","article-title":"Non-conservativity of Coquand's calculus with respect to higher-order intuitionistic logic","author":"Berardi","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB2","article-title":"The semantics of CLEAR, a specification language","volume":"Vol. 86","author":"Burstall","year":"1980"},{"key":"10.1016\/0890-5401(91)90062-7_BIB3","article-title":"Pebble, a kernel language for modules and abstract data types","volume":"Vol. 173","author":"Burstall","year":"1984"},{"key":"10.1016\/0890-5401(91)90062-7_BIB4","series-title":"A set-theoretic setting for structuring theories in proof development","author":"Burstall","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB5","series-title":"Proceedings, Internat. Conf. on Fifth Generation Computer Systems","article-title":"Programming with modules as typed functional programming","author":"Burstall","year":"1984"},{"key":"10.1016\/0890-5401(91)90062-7_BIB6","series-title":"Proceedings, 20th IBM Computer Science Symposium","article-title":"Research in interactive theorem proving at Edinburgh University","author":"Burstall","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB7","series-title":"talk given in Workshop on Programming Logic","article-title":"An approach to program specification and development in constructions","author":"Burstall","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB8","doi-asserted-by":"crossref","DOI":"10.1016\/0168-0072(86)90053-9","article-title":"Contextual category and generalized algebraic theories","volume":"32","author":"Cartmell","year":"1986","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/0890-5401(91)90062-7_BIB9","volume":"Vol. 1","author":"Curry","year":"1958"},{"key":"10.1016\/0890-5401(91)90062-7_BIB10","doi-asserted-by":"crossref","DOI":"10.1016\/0890-5401(89)90068-0","article-title":"Domain Theoretic Models of Polymorphism","author":"Coquand","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB11","series-title":"EUROCAL '85","article-title":"Constructions: A higher order proof system for mechanizing mathematics","volume":"Vol. 203","author":"Coquand","year":"1985"},{"issue":"Nos. 2\/3","key":"10.1016\/0890-5401(91)90062-7_BIB12","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","article-title":"The calculus of constructions","volume":"76","author":"Coquand","year":"1988","journal-title":"Inform. and Comput."},{"issue":"No. 1","key":"10.1016\/0890-5401(91)90062-7_BIB13","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/0890-5401(91)90062-7_BIB14","author":"Constable","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB15","article-title":"Une Th\u00e9orie des Constructions","author":"Coquand","year":"1985"},{"key":"10.1016\/0890-5401(91)90062-7_BIB16","series-title":"Proceedings, 1st Annu. Symp. on Logic in Computer Science","article-title":"An analysis of Girard's paradox","author":"Coquand","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB17","series-title":"A calculus of constructions","author":"Coquand","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB18","series-title":"Metamathematical investigations of a calculus of constructions","author":"Coquand","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB19","series-title":"Inductively defined types","author":"Coquand","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB20","series-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","article-title":"A survey of the project AUTOMATH","author":"de Bruijn","year":"1980"},{"key":"10.1016\/0890-5401(91)90062-7_BIB21","author":"Devlin","year":"1979"},{"key":"10.1016\/0890-5401(91)90062-7_BIB22","series-title":"Proceedings, 3rd Annu. Symp. on Logic in Computer Science","article-title":"A categorical semantics of constructions","author":"Ehrhard","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB23","series-title":"talk given in the 3rd Jumelage Meeting on Typed Lambda Calculi","article-title":"A modular proof of strong normalization for the calculus of constructions","author":"Geuvers","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB24","article-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"10.1016\/0890-5401(91)90062-7_BIB25","doi-asserted-by":"crossref","DOI":"10.1016\/0304-3975(86)90044-7","article-title":"The system F of variable types, fifteen years later","volume":"45","author":"Girard","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(91)90062-7_BIB26","author":"Hook","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB27","series-title":"Proceedings, 2nd Annu. Symp. on Logic in Computer Science","article-title":"A framework for defining logics","author":"Harper","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB28","article-title":"Standard ML","author":"Harper","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB29","series-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","article-title":"The formulae-as-types notion of construction","author":"Howard","year":"1980"},{"key":"10.1016\/0890-5401(91)90062-7_BIB30","series-title":"Categories in Computer Science and Logic, Boulder","article-title":"The theory of constructions: Categorical semantics and topos-theoretic models","author":"Hyland","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB31","article-title":"Type checking, universe polymorphism, and typical ambiguity in the calculus of constructions","author":"Harper","year":"1989","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(91)90062-7_BIB32","series-title":"The Brouwer Symposium","article-title":"The effective topos","author":"Hyland","year":"1982"},{"key":"10.1016\/0890-5401(91)90062-7_BIB33","article-title":"A small complete category","author":"Hyland","year":"1987","journal-title":"Ann. Pure Appl. Logic"},{"key":"10.1016\/0890-5401(91)90062-7_BIB34","article-title":"Combinatory Reduction Systems","volume":"Vol. 127","author":"Klop","year":"1980"},{"issue":"Nos. 2\/3","key":"10.1016\/0890-5401(91)90062-7_BIB35","doi-asserted-by":"crossref","first-page":"278","DOI":"10.1016\/0890-5401(88)90011-9","article-title":"Pebble, a kernel language for modules and abstract data types","volume":"76","author":"Lampson","year":"1988","journal-title":"Inform. and Comput."},{"key":"10.1016\/0890-5401(91)90062-7_BIB36","series-title":"Proceedings, Fourth Symp. on Logic in Computer Science","article-title":"Stratified polymorphism","author":"Leivant","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB37","author":"Levy","year":"1979"},{"key":"10.1016\/0890-5401(91)90062-7_BIB38","author":"Longo","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB39","author":"Luo","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB40","author":"Luo","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB41","author":"Luo","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB42","series-title":"Proceedings, Fourth Annu. Symp. on Logic in Computer Science","article-title":"ECC, an extended calculus of constructions","author":"Luo","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB43","article-title":"An extended calculus of constructions","author":"Luo","year":"1989","journal-title":"thesis"},{"key":"10.1016\/0890-5401(91)90062-7_BIB44","series-title":"Proceedings, 13th Principles of Programming Languages","article-title":"Using dependent types to express modular structure","author":"MacQueen","year":"1986"},{"key":"10.1016\/0890-5401(91)90062-7_BIB45","author":"Meseguer","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB46","series-title":"Proceedings, 15th Principles of Programming Languages","article-title":"The essence of ML","author":"Mitchell","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB47","series-title":"An intuitionistic theory of types","author":"Martin-L\u00f6f","year":"1972"},{"key":"10.1016\/0890-5401(91)90062-7_BIB48","series-title":"Logic Colloquium '73","article-title":"An intuitionistic theory of types: Predicative part","author":"Martin-L\u00f6f","year":"1973"},{"key":"10.1016\/0890-5401(91)90062-7_BIB49","author":"Martin-L\u00f6f","year":"1984","journal-title":"Intuitionistic Type Theory"},{"key":"10.1016\/0890-5401(91)90062-7_BIB50","series-title":"Proceedings, 12th Principles of Programming Languages","article-title":"Abstract types have existential type","author":"Mitchell","year":"1985"},{"key":"10.1016\/0890-5401(91)90062-7_BIB51","series-title":"The PER-model as internal category with all small products","author":"Moggi","year":"1985"},{"key":"10.1016\/0890-5401(91)90062-7_BIB52","series-title":"Programming in Martin-L\u00f6f's type theory: An introduction","author":"Nordstr\u00f6m","year":"1990"},{"key":"10.1016\/0890-5401(91)90062-7_BIB53","series-title":"Notes about the extensions of ECC for including inductive (recursive) types","author":"Ore","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB54","author":"Paulson","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB55","series-title":"Summer Conf. on Category Theory and Computer Science","article-title":"Polymorphism is set theoretic, constructively","author":"Pitts","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB56","series-title":"The theory of LEGO","author":"Pollack","year":"1989"},{"key":"10.1016\/0890-5401(91)90062-7_BIB57","author":"Pottinger","year":"1987"},{"key":"10.1016\/0890-5401(91)90062-7_BIB58","author":"Prawitz","year":"1965"},{"key":"10.1016\/0890-5401(91)90062-7_BIB59","article-title":"Towards a theory of type structure","volume":"Vol. 19","author":"Reynolds","year":"1974"},{"key":"10.1016\/0890-5401(91)90062-7_BIB60","series-title":"Information Processing '83","article-title":"Types, abstraction and parameter polymorphism","author":"Reynolds","year":"1983"},{"key":"10.1016\/0890-5401(91)90062-7_BIB61","article-title":"Polymorphism is not set-theoretic","volume":"Vol. 173","author":"Reynolds","year":"1984"},{"key":"10.1016\/0890-5401(91)90062-7_BIB62","author":"Reynolds","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB63","series-title":"8th Colloquium on Trees in Algebra and Programming","article-title":"Structured theories in LCF","author":"Sannella","year":"1983"},{"key":"10.1016\/0890-5401(91)90062-7_BIB64","article-title":"Locally cartesian closed categories and type theory","volume":"95","author":"Seely","year":"1984"},{"key":"10.1016\/0890-5401(91)90062-7_BIB65","article-title":"Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions","author":"Streicher","year":"1988","journal-title":"Ph.D. dissertation"},{"key":"10.1016\/0890-5401(91)90062-7_BIB66","series-title":"Logic Colloquium","article-title":"A realizability interpretation of the theory of species","volume":"Vol. 453","author":"Tait","year":"1975"},{"key":"10.1016\/0890-5401(91)90062-7_BIB67","series-title":"Stud. Logic 81","article-title":"Proof theory","author":"Takeuti","year":"1975"},{"key":"10.1016\/0890-5401(91)90062-7_BIB68","series-title":"Theories, mathematical structures, and strong sums","author":"Taylor","year":"1988"},{"key":"10.1016\/0890-5401(91)90062-7_BIB69","article-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","volume":"Vol. 344","author":"Troelstra","year":"1973"},{"key":"10.1016\/0890-5401(91)90062-7_BIB70","article-title":"The Language Theory of Automath","author":"van Daalen","year":"1980"},{"key":"10.1016\/0890-5401(91)90062-7_BIB71","article-title":"Formalization of classical mathematics in AUTOMATH","volume":"249","author":"Zucker","year":"1975"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540191900627?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540191900627?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,2,1]],"date-time":"2019-02-01T13:25:35Z","timestamp":1549027535000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0890540191900627"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991,1]]},"references-count":71,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1991,1]]}},"alternative-id":["0890540191900627"],"URL":"https:\/\/doi.org\/10.1016\/0890-5401(91)90062-7","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[1991,1]]}}}