{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,13]],"date-time":"2022-12-13T12:29:34Z","timestamp":1670934574458},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631729","type":"print"},{"value":"9783540692010","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63172-0_45","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T23:16:08Z","timestamp":1330298168000},"page":"275-296","source":"Crossref","is-referenced-by-count":13,"title":["Coercive subtyping in type theory"],"prefix":"10.1007","author":[{"given":"Zhaohui","family":"Luo","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"D. Aspinall and A. Compagnoni. Subtyping dependent types. Proc. of LICS96, 1996. To appear.","DOI":"10.1109\/LICS.1996.561307"},{"key":"17_CR2","unstructured":"P. Aczel. Simple overloading for type theories. Draft, 1994."},{"key":"17_CR3","unstructured":"A. Bailey. Lego with implicit coercions. 1996. Draft."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance and explicit coercion. Information and Computation, 93, 1991.","DOI":"10.1016\/0890-5401(91)90055-7"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"M.J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-68952-9"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"K. Bruce and G. Longo. A modest model of records, inheritance, and bounded quantification. Information and Computation, 87, 1990.","DOI":"10.1016\/0890-5401(90)90062-M"},{"key":"17_CR7","unstructured":"R. Burstall and J. McKinna. Deliverables: a categorical approach to program development in type theory. LFCS report ECS-LFCS-92-242, Dept of Computer Science, University of Edinburgh, 1992."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"R. Burstall. Extended Calculus of Constructions as a specification language. In R. Bird and C. Morgan, editors, Mathematics of Program Construction, 1993. Invited talk.","DOI":"10.1007\/3-540-56625-2_1"},{"key":"17_CR9","unstructured":"R.L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Pretice-Hall, 1986."},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"L. Cardelli. Type-checking dependent types and subtypes. Lecture Notes in Computer Science, 306, 1988.","DOI":"10.1007\/3-540-19129-1_2"},{"key":"17_CR11","unstructured":"Th. Coquand. Pattern matching with dependent types. Talk given at the BRA workshop on Proofs and Types, Bastad, 1992."},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Th. Coquand and Ch. Paulin-Mohring. Inductively defined types. Lecture Notes in Computer Science, 417, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17, 1985.","DOI":"10.1145\/6041.6042"},{"key":"17_CR14","unstructured":"G. Dowek et al. The Coq Proof Assistent: User's Guide (version 5.6). INRIA-Rocquencourt and CNRS-ENS Lyon, 1991."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"P. Dybjer. Inductive sets and families in Martin-L\u00f6f's type theory and their set-theoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks. Cambridge University Press, 1991.","DOI":"10.1017\/CBO9780511569807.012"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"H. Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, 1994.","DOI":"10.1007\/BFb0014053"},{"key":"17_CR17","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Proc. 2nd Ann. Symp. on Logic in Computer Science. IEEE, 1987."},{"key":"17_CR18","unstructured":"G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping. In Proc. of LICS'95, 1995."},{"key":"17_CR19","unstructured":"Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh, 1992."},{"key":"17_CR20","volume-title":"ECC, an extended calculus of constructions","author":"Z. Luo","year":"1989","unstructured":"Z. Luo. ECC, an extended calculus of constructions. In Proc. of the Fourth Ann. Symp. on Logic in Computer Science, Asilomar, California, U.S.A., June 1989. IEEE."},{"key":"17_CR21","unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Also as Report CST-65-90\/ECS-LFCS-90-118, Department of Computer Science, University of Edinburgh."},{"issue":"1","key":"17_CR22","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1016\/0890-5401(91)90062-7","volume":"90","author":"Z. Luo","year":"1991","unstructured":"Z. Luo. A higher-order calculus and theory abstraction. Information and Computation, 90(1): 107\u2013137, 1991.","journal-title":"Information and Computation"},{"key":"17_CR23","unstructured":"Z. Luo. A unifying theory of dependent types: the schematic approach. Proc. of Symp. on Logical Foundations of Computer Science (Logic at Tver'92), LNCS 620, 1992. Also as LFCS Report ECS-LFCS-92-202, Dept. of Computer Science, University of Edinburgh."},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"Z. Luo. Program specification and data refinement in type theory. Mathematical Structures in Computer Science, 3(3), 1993.","DOI":"10.1017\/S0960129500000256"},{"key":"17_CR25","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Oxford University Press, 1994."},{"key":"17_CR26","unstructured":"Z. Luo. Developing reuse technology in proof engineering. Proceedings of AISB95, Workshop on Automated Reasoning: bridging the gap between theory and practice, Sheffield, U.K., April 1995."},{"key":"17_CR27","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory. Bibliopolis, 1984."},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"P. Martin-L\u00f6f. Analytic and synthetic judgements in type theory. In P. Parrini, editor, Kant and Contemporary Epistemology. Kluwer Accademic Publishers, 1994.","DOI":"10.1007\/978-94-011-0834-8_5"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"L. Magnusson and B. Nordstr\u00f6m. The ALF proof editor and its proof engine. In Types for Proof and Programs, LNCS, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"17_CR30","unstructured":"B. Nordstr\u00f6m, K. Petersson, and J. Smith. Programming in Martin-L\u00f6f's Type Theory: An Introduction. Oxford University Press, 1990."},{"key":"17_CR31","unstructured":"F. Pfenning. Refinement types for logical frameworks. Preliminary Proceedings of BRA Workshop on Types and Proofs, 1993."},{"key":"17_CR32","unstructured":"R. Pollack. Implicit syntax. In the preliminary Proceedings of the 1st Workshop on Logical Frameworks, 1990."},{"key":"17_CR33","unstructured":"R. Pollack. The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. PhD thesis, Edinburgh University, 1994."},{"key":"17_CR34","doi-asserted-by":"crossref","unstructured":"A. Saibi. Typing algorithm in type theory with inheritance. Draft, 1996.","DOI":"10.1145\/263699.263742"}],"container-title":["Computer Science Logic","Lecture Notes in Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63172-0_45.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:05Z","timestamp":1605647825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63172-0_45"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631729","9783540692010"],"references-count":34,"URL":"http:\/\/dx.doi.org\/10.1007\/3-540-63172-0_45","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"published":{"date-parts":[[1997]]}}}