{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,1]],"date-time":"2026-02-01T06:30:46Z","timestamp":1769927446370,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540617808","type":"print"},{"value":"9783540707226","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61780-9_58","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:25:25Z","timestamp":1330295125000},"page":"1-15","source":"Crossref","is-referenced-by-count":10,"title":["Implicit coercions in type systems"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Barthe","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"1_CR1","unstructured":"P. Aczel. A notion of class for type theory. Note, 1995."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"D. Aspinall and A. Compagnoni. Subtyping dependent types. In Proceedings of LICS'96. IEEE Computer Society Press, 1996. To appear.","DOI":"10.1109\/LICS.1996.561307"},{"key":"1_CR3","unstructured":"A. Bailey. Lego with classes. Note, 1995."},{"key":"1_CR4","unstructured":"G. Barthe. Formalising algebra in type theory: fundamentals and applications to group theory. Manuscript. An earlier version appeared as technical report CSI-R9508, University of Nijmegen, under the title \u2018Formalising mathematics in type theory: fundamentals and case studies', 1995."},{"key":"1_CR5","unstructured":"G. Betarte and A. Tasistro. Extension of Martin-L\u00f6f's theory of types with record types and subtyping: motivation, rules and type checking. Manuscript, 1995."},{"key":"1_CR6","unstructured":"G. Betarte and A. Tasistro. Formalisation of systems of algebras using dependent record types and subtyping: an example. Manuscript, 1995."},{"key":"1_CR7","volume-title":"Implementing Mathematics with the NuPrl Development System","author":"R.L. Constable","year":"1986","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, W.R. Cleaveland, J.F. Cremer, R.W. Harper, D.J. Howe, T.B. Knoblock, N.P. Mendler, P. Panangaden, J.T. Sasaki, and S.F. Smith. Implementing Mathematics with the NuPrl Development System. Prentice-Hall, inc., Englewood Cliffs, New Jersey, first edition, 1986.","edition":"first edition"},{"key":"1_CR8","series-title":"volume 133 of Studies in Logic and the Foundations of Mathematics","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1016\/S0049-237X(08)70231-3","volume-title":"Selected papers on Automath","author":"N.G. Bruijn de","year":"1994","unstructured":"N.G. de Bruijn. The mathematical vernacular, a language for mathematics with typed sets. In R. Nederpelt, H. Geuvers, and R. de Vrijer, editors, Selected papers on Automath, volume 133 of Studies in Logic and the Foundations of Mathematics, pages 865\u2013935. North-Holland, Amsterdam, 1994."},{"key":"1_CR9","unstructured":"C.A. Gunter and J.C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics and Language Design. The MIT Press, 1994."},{"key":"1_CR10","doi-asserted-by":"crossref","unstructured":"P. Hudak, S.L. Peyton Jones, P.L. Wadler, Arvind, B. Boutel, J. Fairbairn, J. Fasel, K. Guzman, K. Hammond, J. Hughes, T. Johnsson, R. Kieburtz, R.S. Nikhil, W. Partain, and J. Peterson. Report on the functional programming language Haskell, version 1.2. Special Issue of SIGPLAN Notices, 27, 1992.","DOI":"10.1145\/130697.130699"},{"key":"1_CR11","unstructured":"M. Jones. Introduction to Gofer. Included as part of the Gofer distribution. Available by anonymous ftp from nebula.cs.yale.edu in the directory pub\/haskell\/gofer, 1991."},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"M. Jones. A system of constructor classes: overloading and implicit higher-order polymorphism. Journal of Functional Programming, pages 1\u201325, January 1995.","DOI":"10.1017\/S0956796800001210"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Number 11 in International Series of Monographs on Computer Science. Oxford University Press, 1994.","DOI":"10.1093\/oso\/9780198538356.001.0001"},{"key":"1_CR14","unstructured":"Z. Luo. Coercive subtyping. Draft, 1995."},{"key":"1_CR15","unstructured":"F. Pfenning. Refinement types for logical frameworks. In H. Geuvers, editor, Informal Proceedings of TYPES'93, pages 285\u2013299, 1993. Available from http:\/\/www.dcs.ed.ac.uk\/lfcsinfo\/research\/types-bra\/proc\/index.html."},{"key":"1_CR16","unstructured":"R. Pollack. Implicit syntax. In G. Huet and G. Plotkin, editors, Informal Proceedings of First Workshop on Logical Frameworks, Antibes, May 1990."},{"issue":"1","key":"1_CR17","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1006\/inco.1993.1038","volume":"105","author":"L. S. Benthem Jutting van","year":"1993","unstructured":"L. S. van Benthem Jutting. Typing in pure type systems. Information and Computation, 105(1):30\u201341, July 1993.","journal-title":"Information and Computation"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"P. Wadler and S. Blott. How to make ad hoc polymorphism less ad hoc. In Proceedings of POPL'89, pages 60\u201376. ACM Press, 1989.","DOI":"10.1145\/75277.75283"},{"key":"1_CR19","unstructured":"A. Wikstr\u00f6m. Functional Progrmmaming using Standard ML. Interntional Series in Computer Science. Prenctice Hall, 1987."}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61780-9_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,20]],"date-time":"2024-04-20T17:47:40Z","timestamp":1713635260000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61780-9_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540617808","9783540707226"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61780-9_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}