{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,5,7]],"date-time":"2024-05-07T05:58:41Z","timestamp":1715061521096},"reference-count":54,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"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":3638,"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,8]]},"DOI":"10.1016\/s0890-5401(03)00062-2","type":"journal-article","created":{"date-parts":[[2003,6,2]],"date-time":"2003-06-02T23:15:45Z","timestamp":1054595745000},"page":"242-297","source":"Crossref","is-referenced-by-count":16,"title":["Typed operational semantics for higher-order subtyping"],"prefix":"10.1016","volume":"184","author":[{"given":"Adriana","family":"Compagnoni","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Healfdene","family":"Goguen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0890-5401(03)00062-2_BIB1","series-title":"in: ECOOP\u201995","first-page":"145","article-title":"On subtyping and matching","author":"Abadi","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB2","series-title":"A Theory of Objects","author":"Abadi","year":"1996"},{"issue":"4","key":"10.1016\/S0890-5401(03)00062-2_BIB3","doi-asserted-by":"crossref","first-page":"575","DOI":"10.1145\/155183.155231","article-title":"Subtyping recursive types","volume":"15","author":"Amadio","year":"1993","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB4","doi-asserted-by":"crossref","unstructured":"D. Aspinall, A. Compagnoni, Subtyping dependent types, in: 11th Annual Symposium on Logic in Computer Science, July 1996, IEEE, New Brunswick, NJ","DOI":"10.1109\/LICS.1996.561307"},{"issue":"1\u20132","key":"10.1016\/S0890-5401(03)00062-2_BIB5","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1016\/S0304-3975(00)00175-4","article-title":"Subtyping dependent types","volume":"266","author":"Aspinall","year":"2001","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB6","first-page":"117","article-title":"Lambda calculi with types","volume":"vol. 2","author":"Barendregt","year":"1992"},{"issue":"4","key":"10.1016\/S0890-5401(03)00062-2_BIB7","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"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB8","unstructured":"K.B. Bruce, Typing in object-oriented languages: achieving expressiveness and safety, June 1996, Unpublished"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB9","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":"Inf. Comput."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB10","doi-asserted-by":"crossref","unstructured":"K.B. Bruce, J. Mitchell, PER models of subtyping, recursive types and higher-order polymorphism, in: Proceedings of the 19th ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992","DOI":"10.1145\/143165.143230"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB11","series-title":"in: ECOOP\u201995","article-title":"PolyTOIL: a type-safe polymorphic object-oriented language","author":"Bruce","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB12","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1016\/0890-5401(88)90007-7","article-title":"A semantics of multiple inheritance","volume":"76","author":"Cardelli","year":"1988","journal-title":"Inf. Comput."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB13","series-title":"First Conference on Extending Database Technology","article-title":"Types for data-oriented languages","volume":"vol. 303","author":"Cardelli","year":"1988"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB14","unstructured":"L. Cardelli, Notes about F\u03c9<:, October 1990, Unpublished manuscript"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB15","series-title":"Formal Description of Programming Concepts","article-title":"Typeful programming","author":"Cardelli","year":"1991"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB16","unstructured":"L. Cardelli, Extensible records in a pure calculus of subtyping, Research Report 81, DEC Systems Research Center, January 1992, Also in 37"},{"issue":"4","key":"10.1016\/S0890-5401(03)00062-2_BIB17","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. Program."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB18","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0960129500000049","article-title":"Operations on records","volume":"1","author":"Cardelli","year":"1991","journal-title":"Math. Struct. Comput. Sci."},{"issue":"4","key":"10.1016\/S0890-5401(03)00062-2_BIB19","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":"Comput. Surv."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB20","doi-asserted-by":"crossref","unstructured":"G. Chen, Subtyping calculus of constructions, in: Proceedings of Mathematical Foundations of Computer Science, 1997","DOI":"10.1007\/BFb0029962"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB21","unstructured":"A. Compagnoni, H. Goguen, Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997, Inf. Comput., submitted"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB22","series-title":"in: CSL\u201994","article-title":"Decidability of higher-order subtyping with intersection types","volume":"vol. 933","author":"Compagnoni","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB23","doi-asserted-by":"crossref","unstructured":"A.B. Compagnoni, Higher-order subtyping with intersection types, PhD thesis, University of Nijmegen, The Netherlands, January 1995, Supervisor: Prof. Barendregt. ISBN 90-9007860-6","DOI":"10.1007\/BFb0022246"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB24","series-title":"in: Proceedings of Computer Science Logic","article-title":"Anti-symmetry of higher-order subtyping","volume":"vol. 1683","author":"Compagnoni","year":"1999"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB25","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1017\/S0960129500070043","article-title":"Higher-order intersection types and multiple inheritance","volume":"6","author":"Compagnoni","year":"1996","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB26","series-title":"Logical Frameworks","article-title":"An algorithm for testing conversion in type theory","author":"Coquand","year":"1991"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB27","unstructured":"T. Coquand, J. Gallier, A proof of strong normalization for the theory of constructions using a Kripke-like interpretation, in: Workshop on Logical Frameworks \u2013 Preliminary Proceedings, 1990"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB28","series-title":"in: Theory and Practice of Software Development 97","article-title":"An applicative module calculus","author":"Courant","year":"1997"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB29","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1017\/S0960129500001134","article-title":"Coherence of subsumption: Minimum typing and type-checking in F\u2a7d","volume":"2","author":"Curien","year":"1992","journal-title":"Math. Struct. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB30","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/0304-3975(86)90043-5","article-title":"A characterisation of F-complete type assignments","volume":"45","author":"Dezani-Ciancaglini","year":"1986","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB31","series-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB32","doi-asserted-by":"crossref","unstructured":"H. Goguen, A typed operational semantics for type theory, PhD thesis, University of Edinburgh, August 1994","DOI":"10.1007\/BFb0014053"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB33","series-title":"in: Types for Proofs and Programs","first-page":"60","article-title":"The metatheory of UTT","volume":"vol. 996","author":"Goguen","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB34","series-title":"in: Proceedings of the International Conference on Typed Lambda Calculi and Applications","first-page":"186","article-title":"Typed operational semantics","volume":"vol. 902","author":"Goguen","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB35","article-title":"A Kripke-style model for the admissibility of structural rule\/s","volume":"vol. 2277","author":"Goguen","year":"2000"},{"issue":"March","key":"10.1016\/S0890-5401(03)00062-2_BIB36","author":"Group","year":"1999","journal-title":"Principles and a Preliminary Design for ML2000"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB37","series-title":"Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design","author":"Gunter","year":"1994"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB38","doi-asserted-by":"crossref","unstructured":"R. Harper, M. Lillibridge, A type-theoretic approach to higher-order modules with sharing, in: Proceedings of the 21st ACM Symposium on Principles of Programming Languages, Portland, OR, January 1994, pp. 123\u2013137","DOI":"10.1145\/174675.176927"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB39","series-title":"in: Proceedings of TYPES\u201996","article-title":"Some algorithmic and proof \u2013 theoretical aspects of coercive subtyping","volume":"vol. 1512","author":"Jones","year":"1996"},{"issue":"1","key":"10.1016\/S0890-5401(03)00062-2_BIB40","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1017\/S0956796800001210","article-title":"A system of constructor classes: overloading and implicit higher-order polymorphism","volume":"5","author":"Jones","year":"1995","journal-title":"J. Funct. Prog."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB41","series-title":"in: Proceedings of the 22nd Symposium on Principles of Programming Languages","first-page":"142","article-title":"Applicative functors and fully transparent higher-order modules","author":"Leroy","year":"1995"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB42","doi-asserted-by":"crossref","unstructured":"D. MacQueen, Using dependent types to express modular structure, in: Proceedings of the 13th ACM Symposium on the Principles of Programming Languages, 1986","DOI":"10.1145\/512644.512670"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB43","unstructured":"P. Martin-L\u00f6f, An intuitionistic theory of types, 1972, Unpublished manuscript"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB44","series-title":"in: Proceedings of the International Conference on Typed Lambda Calculi and Applications","first-page":"289","article-title":"Pure type systems formalized","volume":"vol. 664","author":"McKinna","year":"1993"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB45","series-title":"Handbook of Theoretical Computer Science","article-title":"Type systems for programming languages","author":"Mitchell","year":"1990"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB46","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell, Toward a typed foundation for method specialization and inheritance, in: Proceedings of the 17th ACM Symposium on Principles of Programming Languages, January 1990, pp. 109\u2013124","DOI":"10.1145\/96709.96719"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB47","doi-asserted-by":"crossref","unstructured":"J.C. Mitchell, F. Honsell, K. Fisher, A lambda calculus of objects and method specialization, in: 1993 IEEE Symposium on Logic in Computer Science, June 1993","DOI":"10.1109\/LICS.1993.287603"},{"issue":"1\u20132","key":"10.1016\/S0890-5401(03)00062-2_BIB48","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1016\/S0304-3975(96)00096-5","article-title":"Higher-order subtyping","volume":"176","author":"Pierce","year":"1997","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB49","unstructured":"B.C. Pierce, Programming with intersection types and bounded polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science technical report CMU-CS-91-205"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB50","unstructured":"C. Russo, Types for modules. PhD thesis, University of Edinburgh, June 1998"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB51","series-title":"Semantics of Type Theory: Correctness, Completeness and Independence Results","author":"Streicher","year":"1991"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB52","doi-asserted-by":"crossref","DOI":"10.2307\/2271658","article-title":"Intensional interpretation of functionals of finite type I","volume":"32","author":"Tait","year":"1967","journal-title":"J. Symbolic Logic"},{"key":"10.1016\/S0890-5401(03)00062-2_BIB53","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1006\/inco.1995.1057","article-title":"Parallel reductions in \u03bb-calculus","volume":"118","author":"Takahashi","year":"1995","journal-title":"Inf. Comput."},{"key":"10.1016\/S0890-5401(03)00062-2_BIB54","series-title":"in: Proceedings of the IEEE Symposium on Logic in Computer Science","first-page":"37","article-title":"Complete type inference for simple objects","volume":"vol. 25","author":"Wand","year":"1987"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000622?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0890540103000622?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,3,20]],"date-time":"2020-03-20T19:34:20Z","timestamp":1584732860000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0890540103000622"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":54,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["S0890540103000622"],"URL":"https:\/\/doi.org\/10.1016\/s0890-5401(03)00062-2","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}