{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T05:18:22Z","timestamp":1754111902793},"reference-count":63,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[1997,4,1]],"date-time":"1997-04-01T00:00:00Z","timestamp":859852800000},"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":5951,"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":[[1997,4]]},"DOI":"10.1016\/s0304-3975(96)00096-5","type":"journal-article","created":{"date-parts":[[2003,4,23]],"date-time":"2003-04-23T19:53:40Z","timestamp":1051127620000},"page":"235-282","source":"Crossref","is-referenced-by-count":32,"title":["Higher-order subtyping"],"prefix":"10.1016","volume":"176","author":[{"given":"Benjamin","family":"Pierce","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(96)00096-5_BIB1","series-title":"A Theory of Objects","author":"Abadi","year":"1996"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB2","article-title":"The Lambda Calculus: Its Syntax and Semantics","volume":"Vol. 103","author":"Barendregt","year":"1984"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB3_1","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","article-title":"Inheritance as implicit coercion","volume":"93","author":"Breazu-Tannen","year":"1991","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB3_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"issue":"2","key":"10.1016\/S0304-3975(96)00096-5_BIB4_1","doi-asserted-by":"crossref","DOI":"10.1017\/S0956796800001039","article-title":"A paradigmatic object-oriented programming language: design, static typing and semantics","volume":"4","author":"Bruce","year":"1994","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB4_2","series-title":"POPL","article-title":"A preliminary version: Safe type checking in a statically typed object-oriented programming language","author":"Bruce","year":"1993"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB5_1","doi-asserted-by":"crossref","first-page":"196","DOI":"10.1016\/0890-5401(90)90062-M","article-title":"A modest model of records, inheritance, and bounded quantification","volume":"87","author":"Bruce","year":"1990","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB5_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB5_3","series-title":"Proc. IEEE Symp. on Logic in Computer Science","year":"1988"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB6","series-title":"Proc. 19th ACM Symp. on Principles of Programming Languages","article-title":"PER models of subtyping, recursive types and higher-order polymorphism","author":"Bruce","year":"1992"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB7","series-title":"4th Internat. Conf. on Functional Programming Languages and Computer Architecture","first-page":"273","article-title":"F-bounded quantification for object-oriented programming","author":"Canning","year":"1989"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB8_1","series-title":"Semantics of Data Types","first-page":"51","article-title":"A semantics of multiple inheritance","volume":"Vol. 173","author":"Cardelli","year":"1984"},{"issue":"2\/3","key":"10.1016\/S0304-3975(96)00096-5_BIB8_2","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1016\/0890-5401(88)90007-7","volume":"76","author":"Cardelli","year":"1988","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB9","series-title":"Proc. 15th ACM Symp. on Principles of Programming Languages","first-page":"70","article-title":"Structural subtyping and the notion of power type","author":"Cardelli","year":"1988"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB10","series-title":"Notes about F\u03c9<:","author":"Cardelli","year":"1990"},{"issue":"4","key":"10.1016\/S0304-3975(96)00096-5_BIB11_1","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1017\/S0956796800000198","article-title":"A semantic basis for Quest","volume":"1","author":"Cardelli","year":"1991","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB11_2","series-title":"ACM Conf. on Lisp and Functional Programming","author":"Cardelli","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB11_3","author":"Cardelli","year":"1990","journal-title":"DEC SRC Research Report 55"},{"issue":"1\u20132","key":"10.1016\/S0304-3975(96)00096-5_BIB12_1","doi-asserted-by":"crossref","first-page":"4","DOI":"10.1006\/inco.1994.1013","article-title":"An extension of system F with subtyping","volume":"109","author":"Cardelli","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB12_2","series-title":"TACS '91","first-page":"750","author":"Cardelli","year":"1991"},{"issue":"4","key":"10.1016\/S0304-3975(96)00096-5_BIB13","doi-asserted-by":"crossref","DOI":"10.1145\/6041.6042","article-title":"On understanding types, data abstraction, and polymorphism","volume":"17","author":"Cardelli","year":"1985","journal-title":"Computing Surveys"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB14","series-title":"Logic and Computer Science","first-page":"19","article-title":"Two extensions of Curry's type inference system","author":"Cardone","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB15","series-title":"Proc. 21st ACM Symp. on Principles of Programming Languages (POPL)","article-title":"Decidable bounded quantification","author":"Castagna","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB16","series-title":"Proc. 22nd ACM Symp. on Principles of Programming Languages (POPL)","article-title":"Corrigendum: decidable bounded quantification","author":"Castagna","year":"1995"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB17","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. Symbolic Logic"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB18_1","article-title":"Subtyping in F\u039b\u03c9 is decidable","author":"Compagnoni","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB18_2","series-title":"Proc. Computer Science Logic","article-title":"Decidability of higher-order subtyping with intersection types","author":"Compagnoni","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB19","article-title":"Higher-order subtyping with intersection types","author":"Compagnoni","year":"1995"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB20_1","article-title":"Multiple inheritance via intersection types","author":"Compagnoni","year":"1995","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB20_2","author":"Compagnoni","year":"1993","journal-title":"University of Edinburgh Tech. Report ECS-LFCS-93-275 and Catholic University Nijmegen computer science Tech. Report 93-18"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB21_1","series-title":"17th Annual ACM Symp. on Principles of Programming Languages","first-page":"125","article-title":"Inheritance is not subtyping","author":"Cook","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB21_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB22","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":"1978","journal-title":"Arch. Math. Logik"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB23","series-title":"Theoretical Aspects of Computer Software","first-page":"731","article-title":"Subtyping+extensionality: confluence of \u03b2\u03b7-reductions in F","volume":"Vol. 526","author":"Curien","year":"1991"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB24_1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1017\/S0960129500001134","article-title":"Coherence of subsumption: minimum typing and type-checking in F","volume":"2","author":"Curien","year":"1992","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB24_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB25","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(96)00096-5_BIB26_1","article-title":"Proof theoretic studies about a minimal type system integrating inclusion and parametric polymorphism","author":"Ghelli","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB26_2","unstructured":"Tech. Report TD-6\/90, Dipartimento di Informatica, Universit\u00e0 di Pisa."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB28","series-title":"Typed Lambda Calculus and Applications","article-title":"Recursive types are not conservative over F\u2a7d","author":"Ghelli","year":"1993"},{"issue":"1","key":"10.1016\/S0304-3975(96)00096-5_BIB29","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1016\/0304-3975(94)00037-J","article-title":"Divergence of F\u2a7d type checking","volume":"139","author":"Ghelli","year":"1995","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB30","doi-asserted-by":"crossref","unstructured":"G. Ghelli and B. Pierce, Bounded existentials and minimal typing, Theoret. Comput. Sci. to appear.","DOI":"10.1016\/S0304-3975(96)00300-3"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB31","article-title":"Interpr\u00e9tation fonctionelle et \u00e9limination des coupures de l'arithm\u00e9tique d'ordre sup\u00e9rieur","author":"Girard","year":"1972"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB32","article-title":"Proofs and Types","volume":"Vol. 7","author":"Girard","year":"1989"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB33_1","doi-asserted-by":"crossref","DOI":"10.1017\/S0956796800001490","article-title":"A unifying type-theoretic framework for objects","author":"Hofmann","year":"1995","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB33_2","series-title":"Symp. on Theoretical Aspects of Computer Science","first-page":"251","author":"Hofmann","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB33_3","article-title":"An abstract view of objects and subtyping (preliminary report)","author":"Hofmann","year":"1992"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB34","series-title":"Proc. ACM Conf. on Lisp and Functional Programming","first-page":"174","article-title":"Bounded quantifiers have interval models","author":"Martini","year":"1988"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB35_1","series-title":"Proc. 17th ACM Symp. on Principles of Programming Languages","first-page":"109","article-title":"Toward a typed foundation for method specialization and inheritance","author":"Mitchell","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB35_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB36","series-title":"Logic and Computer Science","volume":"Vol. 31","year":"1990"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB37_1","article-title":"Programming with intersection types and bounded polymorphism","author":"Pierce","year":"1991"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB37_2","unstructured":"available as School of Computer Science Tech. Report CMU-CS-91-205."},{"issue":"1","key":"10.1016\/S0304-3975(96)00096-5_BIB39_1","doi-asserted-by":"crossref","first-page":"131","DOI":"10.1006\/inco.1994.1055","article-title":"Bounded quantification is undecidable","volume":"112","author":"Pierce","year":"1994","journal-title":"Inform. and Comput."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB39_2","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","year":"1994"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB39_3","unstructured":"a preliminary version appeared in: POPL '92."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB41_1","article-title":"Statically typed friendly functions via partially abstract types","author":"Pierce","year":"1993"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB41_2","unstructured":"also available as INRIA-Rocquencourt Rapport de Recherche No. 1899."},{"issue":"2","key":"10.1016\/S0304-3975(96)00096-5_BIB43_1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1017\/S0956796800001040","article-title":"Simple type-theoretic foundations for object-oriented programming","volume":"4","author":"Pierce","year":"1994","journal-title":"J. Funct. Programming"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB43_2","series-title":"Principles of Programming Languages","author":"Pierce","year":"1993"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB43_3","unstructured":"Object-oriented programming without recursive types, University of Edinburgh Tech. Report ECS-LFCS-92-225."},{"key":"10.1016\/S0304-3975(96)00096-5_BIB45","series-title":"Proc. Colloque sur la Programmation","first-page":"408","article-title":"Towards a theory of type structure","volume":"Vol. 17","author":"Reynolds","year":"1974"},{"key":"10.1016\/S0304-3975(96)00096-5_BIB46","article-title":"Pure type systems with definitions","author":"Severi","year":"1993"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397596000965?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397596000965?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,4,26]],"date-time":"2019-04-26T17:58:13Z","timestamp":1556301493000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397596000965"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,4]]},"references-count":63,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1997,4]]}},"alternative-id":["S0304397596000965"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(96)00096-5","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[1997,4]]}}}