{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:56:42Z","timestamp":1725487002804},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540656999"},{"type":"electronic","value":"9783540490999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-49099-x_8","type":"book-chapter","created":{"date-parts":[[2007,6,24]],"date-time":"2007-06-24T21:03:21Z","timestamp":1182719001000},"page":"109-127","source":"Crossref","is-referenced-by-count":9,"title":["Constructor Subtyping"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]},{"given":"Maria Jo\u00e3o","family":"Frade","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,3,28]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Cardelli. A theory of objects. Springer-Verlag, 1996.","DOI":"10.1007\/978-1-4419-8598-9"},{"key":"8_CR2","unstructured":"H. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1984."},{"key":"8_CR3","doi-asserted-by":"crossref","unstructured":"H. Barendregt.The impact of the lambda calculus in logic and computer science. Bulletin of Symbolic Logic, 3(2):181\u2013215, June 1997.","DOI":"10.2307\/421013"},{"key":"8_CR4","unstructured":"B. Barras et. al. The Coq Proof Assistant User\u2019s Guide. Version 6.2, May 1998."},{"key":"8_CR5","unstructured":"G. Barthe. Order-sorted inductive types. Information and Computation, 199x. To appear."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"G. Barthe and M.J. Frade. Constructor subtyping. Technical Report UMDITR9807, Department of Computer Science, University of Minho, 1998.","DOI":"10.1007\/3-540-49099-X_8"},{"key":"8_CR7","unstructured":"G. Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computer Science, Chalmers Tekniska H\u00f6gskola, 1998."},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1145\/234313.234418","volume":"28","author":"L. Cardelli","year":"1996","unstructured":"L. Cardelli. Type systems. ACM Computing Surveys, 28(1):263\u2013264, March 1996.","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"8_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"},{"issue":"1","key":"8_CR10","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1006\/inco.1995.1033","volume":"117","author":"G. Castagna","year":"1995","unstructured":"G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. Information and Computation, 117(1):115\u2013135, February 1995.","journal-title":"Information and Computation"},{"key":"8_CR11","unstructured":"A. Compagnoni and H. Goguen. Typed operational semantics for higher order subtyping. Technical Report ECS-LFCS-97-361, University of Edinburgh, July 1997."},{"key":"8_CR12","unstructured":"T. Coquand. Pattern matching with dependent types. In B. Nordstr \u00f6m, editor, Informal proceedings of Logical Frameworks\u201992, pages 66\u201379, 1992."},{"key":"8_CR13","unstructured":"R. Di Cosmo. A brief history of rewriting with extensionality. Presented at the International Summer School on Type Theory and Term Rewriting, Glasgow, September 1996."},{"issue":"3","key":"8_CR14","doi-asserted-by":"crossref","first-page":"315","DOI":"10.1017\/S0960129500000505","volume":"4","author":"R. Cosmo Di","year":"1994","unstructured":"R. Di Cosmo and D. Kesner. Simulating expansions without expansions. Mathematical Structures in Computer Science, 4(3):315\u2013362, September 1994.","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"E. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of theoretical computer science, volume B, pages 995\u20131072. Elsevier Publishing, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"8_CR16","unstructured":"N. Ghani. Adjoint rewriting. PhD thesis, Laboratory for the Foundations of Computer Science, University of Edinburgh, 1995."},{"key":"8_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1007\/BFb0055070","volume-title":"Proceedings of ICALP'98","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'98, volume 1443 of Lecture Notes in Computer Science, pages 397\u2013408. Springer-Verlag, 1998."},{"issue":"3","key":"8_CR18","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1017\/S0960129500000517","volume":"4","author":"J. Goguen","year":"1994","unstructured":"J. Goguen and R. Diaconescu. An Oxford survey of order sorted algebra. Mathematical Structures in Computer Science, 4(3):363\u2013392, September 1994.","journal-title":"Mathematical Structures in Computer Science"},{"key":"8_CR19","unstructured":"H. Hosoya, B. Pierce, and D.N. Turner. Subject reduction fails in Java. Message to the TYPES mailing list, 1998."},{"issue":"2","key":"8_CR20","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","volume":"5","author":"C.B. Jay","year":"1995","unstructured":"C.B. Jay and N. Ghani. The virtues of eta-expansion. Journal of Functional Programming, 5(2):135\u2013154, April 1995.","journal-title":"Journal of Functional Programming"},{"key":"8_CR21","unstructured":"M.P. Jones. Dictionary-free overloading by partial evaluation. In Proceedings of PEP\u201994, pages 107\u2013117, 1994. University of Melbourne, Australia, Department of Computer Science, Technical Report 94\/9."},{"key":"8_CR22","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":"8_CR23","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/0304-3975(76)90009-8","volume":"2","author":"J.-J. L\u00e9vy","year":"1976","unstructured":"J.-J. L\u00e9vy. An algebraic interpretation of the \u03bb\u03b2\u039a-calculus and a labelled \u03bb-calculus. Theoretical Computer Science, 2:97\u2013114, 1976.","journal-title":"Theoretical Computer Science"},{"key":"8_CR24","unstructured":"Z. Luo. Coercive subtyping. Journal of Logic and Computation, 199x. To appear."},{"key":"8_CR25","doi-asserted-by":"crossref","unstructured":"S. Marlow and P. Wadler. A practical subtyping system for Erlang. In Proceedings of ICFP\u201997, pages 136\u2013149. ACM Press, 1997.","DOI":"10.1145\/258948.258962"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). The MIT Press, 1997.","DOI":"10.7551\/mitpress\/2319.001.0001"},{"key":"8_CR27","unstructured":"J. C. Mitchell, M. Hoang, and B. T. Howard. Labelling techniques and typed fixedpoint operators. In A.D. Gordon and A.M. Pitts, editors, Higher Order Operational Techniques in Semantics, pages 137\u2013174. Cambridge University Press, 1998."},{"key":"8_CR28","unstructured":"J. Peterson and K. Hammond (editors). Haskell 1.4.: A Non-strict, Purely Functional Language, April 1997."},{"key":"8_CR29","unstructured":"F. Pfenning. Refinement types for logical frameworks. In H. Geuvers, editor, Informal Proceedings of TYPES\u201993, pages 285\u2013299, 1993."},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"B.C. Pierce and D.N. Turner. Local type inference. In Proceedings of POPL\u201998, pages 252\u2013265. ACM Press, 1998.","DOI":"10.1145\/268946.268967"},{"key":"8_CR31","unstructured":"F. Pottier. Synth\u00e8se de types en pr\u00e9sence de sous-typage: de la th\u00e9orie la pratique. PhD thesis, Universit \u00e9 Paris VII, 1998."},{"key":"8_CR32","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":"8_CR33","doi-asserted-by":"crossref","unstructured":"H. Xi and F. Pfenning. Dependent types in practical programming. In Proceedings of POPL\u201999. ACM Press, 1999. To appear.","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-49099-X_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T09:33:03Z","timestamp":1556530383000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-49099-X_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540656999","9783540490999"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-49099-x_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}