{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:00:20Z","timestamp":1725487220410},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672579"},{"type":"electronic","value":"9783540464327"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46432-8_2","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T12:22:02Z","timestamp":1184588522000},"page":"17-34","source":"Crossref","is-referenced-by-count":7,"title":["Constructor Subtyping in the Calculus of Inductive Constructions"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Femke","family":"van Raamsdonk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"P. Aczel. An introduction to inductive definitions. In J. Barwise, editor, Handbook of mathematical logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739\u2013782. North-Holland, 1977.","key":"2_CR1","DOI":"10.1016\/S0049-237X(08)71120-0"},{"doi-asserted-by":"crossref","unstructured":"D. Aspinall and A. Compagnoni. Subtyping dependent types. In Proceedings of LICS\u201996, pages 86\u201397. IEEE Computer Society Press, 1996.","key":"2_CR2","DOI":"10.1109\/LICS.1996.561307"},{"unstructured":"B. Barras. Auto-validation d\u2019un syst\u00e8me de preuves avec familles inductives. PhD thesis, Universit\u00e9 Paris 7, 1999.","key":"2_CR3"},{"unstructured":"B. Barras et. al. The Coq Proof Assistant User\u2019s Guide. Version 6.2, May 1998.","key":"2_CR4"},{"key":"2_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/3-540-61780-9_59","volume-title":"Proceedings of TYPES\u201995","author":"G. Barthe","year":"1996","unstructured":"G. Barthe. Implicit coercions in type systems. In S. Berardi and M. Coppo, editors, Proceedings of TYPES\u201995, volume 1158 of Lecture Notes in Computer Science, pages 16\u201335. Springer-Verlag, 1996."},{"key":"2_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1007\/3-540-49019-1_7","volume-title":"Proceedings of FOSSACS\u201999","author":"G. Barthe","year":"1999","unstructured":"G. Barthe. Expanding the cube. In W. Thomas, editor, Proceedings of FOSSACS\u201999, volume 1578 of Lecture Notes in Computer Science, pages 90\u2013103. Springer-Verlag, 1999."},{"issue":"1","key":"2_CR7","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1006\/inco.1998.2751","volume":"149","author":"G. Barthe","year":"1999","unstructured":"G. Barthe. Order-sorted inductive types. Information and Computation, 149(1):42\u201376, February 1999.","journal-title":"Information and Computation"},{"key":"2_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/3-540-49099-X_8","volume-title":"Proceedings of ESOP\u201999","author":"G. Barthe","year":"1999","unstructured":"G. Barthe and M.J. Frade. Constructor subtyping. In D. Swiestra, editor, Proceedings of ESOP\u201999, volume 1576 of Lecture Notes in Computer Science, pages 109\u2013127. Springer-Verlag, 1999."},{"issue":"4","key":"2_CR9","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. ACM Computing Surveys, 17(4):471\u2013522, December 1985.","journal-title":"ACM Computing Surveys"},{"unstructured":"G. Castagna and G. Chen. Dependent types with subtyping and late-bound overloading. Information and Computation, 1999. To appear.","key":"2_CR10"},{"key":"2_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1007\/BFb0029962","volume-title":"Proceedings of MFCS\u201997","author":"G. Chen","year":"1997","unstructured":"G. Chen. Subtyping calculus of constructions. In I. Pr\u00edvara and P. Ruzicka, editors, Proceedings of MFCS\u201997, volume 1295 of Lecture Notes in Computer Science, pages 189\u2013198. Springer-Verlag, 1997."},{"unstructured":"T. Coquand. Metamathematical investigations of a calculus of constructions. In P. Odifreddi, editor, Logic and Computer Science, pages 91\u2013122. Academic Press, 1990.","key":"2_CR12"},{"issue":"1\u20133","key":"2_CR13","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0167-6423(95)00021-6","volume":"26","author":"T. Coquand","year":"1996","unstructured":"T. Coquand. An algorithm for type-checking dependent types. Science of Computer Programming, 26(1\u20133):167\u2013177, May 1996.","journal-title":"Science of Computer Programming"},{"key":"2_CR14","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1007\/3-540-60579-7_2","volume-title":"Proceedings of TYPES\u201994","author":"H. Geuvers","year":"1995","unstructured":"H. Geuvers. A short and flexible proof of strong normalisation for the Calculus of Constructions. In P. Dybjer, B. Nordstr\u00f6m, and J. Smith, editors, Proceedings of TYPES\u201994, volume 996 of Lecture Notes in Computer Science, pages 14\u201338. Springer-Verlag, 1995."},{"issue":"2","key":"2_CR15","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.J. Nederhof. A modular proof of strong normalisation for the Calculus of Constructions. Journal of Functional Programming, 1(2):155\u2013189, April 1991.","journal-title":"Journal of Functional Programming"},{"key":"2_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/3-540-62688-3_35","volume-title":"Proceedings of TLCA\u201997","author":"N. Ghani","year":"1997","unstructured":"N. Ghani. Eta-expansions in dependent type theory\u2014the calculus of constructions. In P. de Groote and J. Hindley, editors, Proceedings of TLCA\u201997, volume 1210 of Lecture Notes in Computer Science, pages 164\u2013180. Springer-Verlag, 1997."},{"unstructured":"E. Gim\u00e9nez. Un calcul de constructions infinies et son application \u00e0 la v\u00e9rification de syst\u00e8mes communicants. PhD thesis, Ecole Normale Superieure de Lyon, 1996.","key":"2_CR17"},{"key":"2_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Proceedings of ICALP\u201998","author":"E. Gim\u00e9nez","year":"1998","unstructured":"E. Gim\u00e9nez. Structural recursive definitions in Type Theory. In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of ICALP\u201998, volume 1443 of Lecture Notes in Computer Science, pages 397\u2013408. Springer-Verlag, 1998."},{"unstructured":"E. Gim\u00e9nez. A tutorial on recursive types in coq. Technical Report RT-0221, INRIA, 1998.","key":"2_CR19"},{"issue":"2","key":"2_CR20","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1016\/0304-3975(92)90302-V","volume":"105","author":"J. Goguen","year":"1992","unstructured":"J. Goguen and J. Meseguer. Order-sorted algebra I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations. Theoretical Computer Science, 105(2):216\u2013273, 1992.","journal-title":"Theoretical Computer Science"},{"unstructured":"M.J.C. Gordon and T.F. Melham, editors. Introduction to HOL: A theorem proving environment for higher-order logic. Cambridge University Press, 1993.","key":"2_CR21"},{"unstructured":"C.A. Gunter and J.C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics and Language Design. The MIT Press, 1994.","key":"2_CR22"},{"key":"2_CR23","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1007\/BFb0039592","volume-title":"Proceedings of the Symposium on Theoretical Aspects of Computer Science","author":"G. Kahn","year":"1987","unstructured":"G. Kahn. Natural semantics. In Proceedings of the Symposium on Theoretical Aspects of Computer Science, volume 247 of Lecture Notes in Computer Science, pages 22\u201339. Springer-Verlag, 1987."},{"key":"2_CR24","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 9:105\u2013130, February 1999.","journal-title":"Journal of Logic and Computation"},{"unstructured":"Z. Luo and R. Pollack. LEGO proof development system: User\u2019s manual. Technical Report ECS-LFCS-92-211, LFCS, University of Edinburgh, May 1992.","key":"2_CR25"},{"doi-asserted-by":"crossref","unstructured":"J. Nordlander. Pragmatic subtyping in polymorphic languages. In Proceedings of ICFP\u201998. ACM Press, 1998.","key":"2_CR26","DOI":"10.1145\/289423.289445"},{"unstructured":"J. Norlander. Reactive Objects and Functional Programming. PhD thesis, Chalmers Tekniska H\u00f6gskola, 1999.","key":"2_CR27"},{"key":"2_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: a generic theorem prover","author":"L. Paulson","year":"1994","unstructured":"L. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994."},{"unstructured":"F. Pfenning. Refinement types for logical frameworks. In H. Geuvers, editor, Informal Proceedings of TYPES\u201993, pages 285\u2013299, 1993.","key":"2_CR29"},{"unstructured":"E. Poll. Subtyping and Inheritance for Inductive Types. In Proceedings of TYPES\u201997 Workshop on Subtyping, inheritance and modular development of proofs, Durham, UK, 1997.","key":"2_CR30"},{"unstructured":"E. Poll. Subtyping and Inheritance for Categorical Datatypes. In Proceedings of Theories of Types and Proofs (TTP)-Kyoto, RIMS Lecture Notes 1023, pages 112\u2013125. Kyoto University Research Insitute for Mathematical Sciences, 1998.","key":"2_CR31"},{"unstructured":"N. Shankar, S. Owre, and J.M. Rushby. The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International, February 1993. Supplemented with the PVS2 Quick Reference Manual, 1997.","key":"2_CR32"},{"unstructured":"M. Steffen. Polarized Higher-order Subtyping. PhD thesis, Department of Computer Science, University of Erlangen, 1997.","key":"2_CR33"},{"issue":"1","key":"2_CR34","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1016\/0168-0072(94)00040-A","volume":"73","author":"J. Terlouw","year":"1995","unstructured":"J. Terlouw. Strong normalization in type systems: a model theoretic approach. Annals of Pure and Applied Logic, 73(1):53\u201378, May 1995.","journal-title":"Annals of Pure and Applied Logic"},{"unstructured":"B. Werner. M\u00e9ta-th\u00e9orie du Calcul des Constructions Inductives. PhD thesis, Universit\u00e9 Paris 7, 1994.","key":"2_CR35"},{"key":"2_CR36","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1007\/3-540-48959-2_27","volume-title":"Proceedings of TLCA\u201999","author":"J. Zwanenburg","year":"1999","unstructured":"J. Zwanenburg. Pure type systems with subtyping. In J.-Y. Girard, editor, Proceedings of TLCA\u201999, volume 1581 of Lecture Notes in Computer Science, pages 381\u2013396. Springer-Verlag, 1999."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46432-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,24]],"date-time":"2020-04-24T21:47:47Z","timestamp":1587764867000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46432-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672579","9783540464327"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/3-540-46432-8_2","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}