{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:59Z","timestamp":1767927839890,"version":"3.49.0"},"reference-count":27,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"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":4337,"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":[[2001,9]]},"DOI":"10.1016\/s0304-3975(00)00175-4","type":"journal-article","created":{"date-parts":[[2002,10,31]],"date-time":"2002-10-31T21:53:12Z","timestamp":1036101192000},"page":"273-309","source":"Crossref","is-referenced-by-count":36,"title":["Subtyping dependent types"],"prefix":"10.1016","volume":"266","author":[{"given":"David","family":"Aspinall","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adriana","family":"Compagnoni","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00175-4_BIB1","doi-asserted-by":"crossref","unstructured":"D. Aspinall, Subtyping with singleton types, Proc. Computer Science Logic, CSL\u201994, Kazimierz, Poland, Lecture Notes in Computer Science, vol. 933, Springer, Berlin, 1995.","DOI":"10.1007\/BFb0022243"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB2","unstructured":"D. Aspinall, Type systems for modular programs and specification, Ph.D. Thesis, Department of Computer Science, University of Edinburgh, 1997."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB3","doi-asserted-by":"crossref","unstructured":"D. Aspinall, A. Compagnoni, Subtyping dependent types, in: E. Clarke (Ed.), Proc. 11th Annual IEEE Symp. on Logic in Computer Science, New Brunswick, New Jersey, IEEE Computer Society Press, Silver Spring, MD, 1996, pp. 86\u201397.","DOI":"10.1109\/LICS.1996.561307"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB4","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1007\/BF00245294","article-title":"Using typed lambda calculus to implement formal systems on a machine","volume":"9","author":"Avron","year":"1992","journal-title":"J. Automat. Reason."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB5","series-title":"Lambda calculi with types, Handbook of Logic in Computer Science","author":"Barendregt","year":"1992"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB6","series-title":"Extension of Martin-L\u00f6f's type theory with record types and subtyping, Proc. 25 Years of Constructive Type Theory","author":"Betarte","year":"1997"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB7","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(00)00175-4_BIB8","article-title":"Typechecking dependent types and subtypes","volume":"vol. 306","author":"Cardelli","year":"1987"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB9","doi-asserted-by":"crossref","unstructured":"L. Cardelli, Structural subtyping and the notion of power type, Conf. Record of the 15th Annual ACM Symp. on Principles of Progamming Languages, San Diego, California, January 13\u201315, ACM SIGACT-SIGPLAN, ACM Press, New York, 1988, pp. 70\u201379.","DOI":"10.1145\/73560.73566"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB10","unstructured":"G. Chen, Subtyping calculus of constructions, Proc. 22nd Internat. Symp. MFCS \u201997, Lecture Notes in Computer Science, vol. 1295, Springer, Berlin, 1997, pp. 189\u2013198."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB11","unstructured":"A. Compagnoni, H. Goguen, Decidability of higher-order subtyping via logical relations, December 1997."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB12","unstructured":"A. Compagnoni, H. Goguen, Typed operational semantics for higher order subtyping, Tech. Rep. ECS-LFCS-97-361, University of Edinburgh, July 1997. Inform. and Comput., to appear."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB13","doi-asserted-by":"crossref","unstructured":"A.B. Compagnoni, Higher-order subtyping with intersection types, Ph.D. Thesis, Nijmegen Catholic University, 1995.","DOI":"10.1007\/BFb0022246"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB14","unstructured":"T. Coquand, Pattern matching with dependent types, Proc. Types for Proofs and Programs, B\u00e5stad, Sweden, 1992, pp. 71\u201383."},{"issue":"2\/3","key":"10.1016\/S0304-3975(00)00175-4_BIB15","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."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB16","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."},{"issue":"1","key":"10.1016\/S0304-3975(00)00175-4_BIB17","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","article-title":"A framework for defining logics","volume":"40","author":"Harper","year":"1993","journal-title":"J. ACM"},{"key":"10.1016\/S0304-3975(00)00175-4_BIB18","unstructured":"G. Longo, K. Milsted. S. Soloviev, A logic of subtyping (extended abstract), Proc. 10th Annual IEEE Symp. on Logic in computer Science, San Diego, California, 26\u201329 June, IEEE Computer Society Press, Silverspring, MD, 1995, pp. 292\u2013299."},{"issue":"1","key":"10.1016\/S0304-3975(00)00175-4_BIB19","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","article-title":"Coercive subtyping","volume":"9","author":"Luo","year":"1999","journal-title":"J. Logic Comput."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB20","unstructured":"I.A. Mason, Hoare's Logic in the LF, Tech. Rep. ECS-LFCS-87-32, LFCS, Department of Computer Science, University of Edinburgh, June 1987."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB21","unstructured":"F. Pfenning, Refinement types for logical frameworks, Informal Proc. 1993 Workshop on Types for Proofs and Programs, May 1993, pp. 315\u2013328."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB22","unstructured":"B.C. Pierce, Programming with intersection types and bounded polymorphism, Ph.D. Thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science Tech. Rep. CMU-CS-91-205."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB23","doi-asserted-by":"crossref","unstructured":"B.C. Pierce, Bounded quantification is undecidable, Proc. 19th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, Albuquerque, New Mexico, January 19\u201322, ACM Press, New York, 1992, pp. 305\u2013315.","DOI":"10.1145\/143165.143228"},{"issue":"2","key":"10.1016\/S0304-3975(00)00175-4_BIB24","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(00)00175-4_BIB25","doi-asserted-by":"crossref","first-page":"689","DOI":"10.1007\/BF01191893","article-title":"Toward formal development of programs from algebraic specifications: parameterisation revisited","volume":"29","author":"Sannella","year":"1992","journal-title":"Acta Inform."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB26","unstructured":"M. Steffen, B. Pierce, Higher-order subtyping, IFIP Working Conf. on Programming Concepts, Methods and Calculi (PROCOMET), June 1994."},{"key":"10.1016\/S0304-3975(00)00175-4_BIB27","unstructured":"J. Zwanenburg, Object-oriented concepts and proof rules: formalization in type theory and implementation in Yarrow, Ph.D. Thesis, Eindhoven University of Technology."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500001754?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500001754?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,10]],"date-time":"2020-01-10T10:29:50Z","timestamp":1578652190000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500001754"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,9]]},"references-count":27,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2001,9]]}},"alternative-id":["S0304397500001754"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00175-4","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2001,9]]}}}