{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:29Z","timestamp":1725562589770},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540221647"},{"type":"electronic","value":"9783540248491"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24849-1_17","type":"book-chapter","created":{"date-parts":[[2010,8,8]],"date-time":"2010-08-08T20:34:24Z","timestamp":1281299664000},"page":"259-275","source":"Crossref","is-referenced-by-count":2,"title":["Coercions in Hindley-Milner Systems"],"prefix":"10.1007","author":[{"given":"Robert","family":"Kie\u00dfling","sequence":"first","affiliation":[]},{"given":"Zhaohui","family":"Luo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Bailey, A.: The Machine-checked Literate Formalisation of Algebra in Type Theory. PhD thesis, University of Manchester (1999)"},{"key":"17_CR2","unstructured":"Barras, B., et al.: The Coq Proof Assistant Reference Manual (Version 6.3.1). INRIARocquencourt (2000)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1016\/0890-5401(91)90055-7","volume":"93","author":"V. Breazu-Tannen","year":"1991","unstructured":"Breazu-Tannen, V., Coquand, T., Gunter, C., \u0160\u010dedrov, A.: Inheritance as implicit coercion. Information and Computation\u00a093, 172\u2013221 (1991); Also in the collection [9]","journal-title":"Information and Computation"},{"issue":"1","key":"17_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1010648911114","volume":"27","author":"P. Callaghan","year":"2001","unstructured":"Callaghan, P., Luo, Z.: An implementation of LF with coercive subtyping and universes. Journal of Automated Reasoning\u00a027(1), 3\u201327 (2001)","journal-title":"Journal of Automated Reasoning"},{"issue":"4","key":"17_CR5","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/6041.6042","volume":"17","author":"L. Cardelli","year":"1985","unstructured":"Cardelli, L., Wegner, P.: On understanding types, data abstraction and polymorphism. Computing Surveys\u00a017(4), 471\u2013522 (1985)","journal-title":"Computing Surveys"},{"key":"17_CR6","unstructured":"Chen, G.: Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, University of Paris VII (1998)"},{"key":"17_CR7","unstructured":"Damas, L.: Type Assignment in Programming Languages. PhD thesis, Laboratory for Foundations of Computer Science, University of Edinburgh, CST-33-85 (1985)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1145\/582153.582176","volume-title":"Ninth Annual Symposium on Principles of Programming Languages (POPL) (Albuquerque, NM)","author":"L. Damas","year":"1982","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programming languages. In: Ninth Annual Symposium on Principles of Programming Languages (POPL) (Albuquerque, NM), January 1982, pp. 207\u2013212. ACM, New York (1982)"},{"key":"17_CR9","series-title":"Foundations of Computing Series","volume-title":"Theoretical Aspects of Object-Oriented Programming, Types, Semantics, and Language Design","author":"C.A. Gunter","year":"1994","unstructured":"Gunter, C.A., Mitchell, J.C.: Theoretical Aspects of Object-Oriented Programming, Types, Semantics, and Language Design. Foundations of Computing Series. MIT Press, Cambridge (1994)"},{"key":"17_CR10","unstructured":"Jones, S.P., Jones, M., Meijer, E.: Type classes: an exploration of the design space (1997)"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Kie\u00dfling, R.: Coercions in Hindley-Milner systems. forthcoming thesis (2004)","DOI":"10.1007\/978-3-540-24849-1_17"},{"issue":"4","key":"17_CR12","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1093\/logcom\/10.4.493","volume":"10","author":"G. Longo","year":"2000","unstructured":"Longo, G., Milsted, K., Soloviev, S.: Coherence and transitivity of subtyping as entailment. Journal of Logic and Computation\u00a010(4), 493\u2013526 (2000)","journal-title":"Journal of Logic and Computation"},{"key":"17_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/3-540-45653-8_17","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"Y. Luo","year":"2001","unstructured":"Luo, Y., Luo, Z.: Coherence and transitivity in coercive subtyping. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, p. 249. Springer, Heidelberg (2001)"},{"issue":"1","key":"17_CR14","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. Journal of Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"17_CR15","unstructured":"Luo, Z., Pollack, R.: LEGO Proof Development System: User\u2019s Manual. LFCS Report ECS-LFCS-92-211, Department of Computer Science, University of Edinburgh (1992)"},{"key":"17_CR16","unstructured":"McKinna, J.: personal communication (2001)"},{"key":"17_CR17","first-page":"175","volume-title":"Tenth Annual Symposium on Principles of Programming Languages (POPL) (Austin, TX)","author":"J.C. Mitchell","year":"1983","unstructured":"Mitchell, J.C.: Coercion and type inference. In: Tenth Annual Symposium on Principles of Programming Languages (POPL) (Austin, TX), January 1983, pp. 175\u2013185. ACM, New York (1983)"},{"issue":"2","key":"17_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1017\/S0956796800000113","volume":"1","author":"J.C. Mitchell","year":"1991","unstructured":"Mitchell, J.C.: Type inference with simple subtypes. Journal of Functional Programming\u00a01(2), 245\u2013286 (1991)","journal-title":"Journal of Functional Programming"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: Proc of POPL 1997 (1997)","DOI":"10.1145\/263699.263742"},{"issue":"1-3","key":"17_CR20","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/S0168-0072(01)00063-X","volume":"113","author":"S. Soloviev","year":"2002","unstructured":"Soloviev, S., Luo, Z.: Coercion completion and conservativity in coercive subtyping. Annals of Pure and Applied Logic\u00a0113(1-3), 297\u2013322 (2002)","journal-title":"Annals of Pure and Applied Logic"},{"key":"17_CR21","series-title":"International Computer Science Series","volume-title":"Type Theory and Functional Programming","author":"S. Thompson","year":"1991","unstructured":"Thompson, S.: Type Theory and Functional Programming. International Computer Science Series. Addison-Wesley, Reading (1991)"},{"key":"17_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1007\/3-540-59451-5_2","volume-title":"Advanced Functional Programming","author":"P. Wadler","year":"1995","unstructured":"Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol.\u00a0925, pp. 24\u201352. Springer, Heidelberg (1995)"},{"key":"17_CR23","first-page":"60","volume-title":"Proceedings of POPL 1989","author":"P. Wadler","year":"1989","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorhism less ad-hoc. In: Proceedings of POPL 1989, January 1989, pp. 60\u201376. ACM, New York (1989)"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24849-1_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:57:39Z","timestamp":1605761859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24849-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540221647","9783540248491"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24849-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}