{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:40:58Z","timestamp":1780994458257,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540710653","type":"print"},{"value":"9783540710677","type":"electronic"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71067-7_23","type":"book-chapter","created":{"date-parts":[[2008,10,3]],"date-time":"2008-10-03T08:55:16Z","timestamp":1223024116000},"page":"278-293","source":"Crossref","is-referenced-by-count":144,"title":["First-Class Type Classes"],"prefix":"10.1007","author":[{"given":"Matthieu","family":"Sozeau","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nicolas","family":"Oury","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"23_CR1","unstructured":"Birtwistle, G.M., Dahl, O.-J., Myhrhaug, B., Nygaard, K.: Simula Begin. Studentlitteratur (Lund, Sweden), Bratt Institut fuer neues Lernen (Goch, FRG), Chartwell-Bratt Ltd (Kent, England) (1979)"},{"key":"23_CR2","first-page":"1","volume-title":"POPL","author":"M.M.T. Chakravarty","year":"2005","unstructured":"Chakravarty, M.M.T., Keller, G., Jones, S.L.P., Marlow, S.: Associated types with class. In: Palsberg, J., Abadi, M. (eds.) POPL, pp. 1\u201313. ACM Press, New York (2005)"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/3-540-44904-3_8","volume-title":"Typed Lambda Calculi and Applications","author":"T. Coquand","year":"2003","unstructured":"Coquand, T., Pollack, R., Takeyama, M.: A logical framework with dependently typed records. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol.\u00a02701, pp. 105\u2013119. Springer, Heidelberg (2003)"},{"key":"23_CR4","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type schemes for functional programs. In: POPL, Albuquerque, New, Mexico, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"23_CR5","first-page":"235","volume-title":"ICFP 2002","author":"B. Gr\u00e9goire","year":"2002","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP 2002, pp. 235\u2013246. ACM Press, New York (2002)"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-540-74464-1_11","volume-title":"Types for Proofs and Programs","author":"F. Haftmann","year":"2007","unstructured":"Haftmann, F., Wenzel, M.: Constructive Type Classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 160\u2013174. Springer, Heidelberg (2007)"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11541868_10","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Huffman","year":"2005","unstructured":"Huffman, B., Matthews, J., White, P.: Axiomatic Constructor Classes in Isabelle\/HOLCF. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 147\u2013162. Springer, Heidelberg (2005)"},{"key":"23_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-46425-5_15","volume-title":"Programming Languages and Systems","author":"M.P. Jones","year":"2000","unstructured":"Jones, M.P.: Type classes with functional dependencies. In: Smolka, G. (ed.) ESOP 2000 and ETAPS 2000. LNCS, vol.\u00a01782, pp. 230\u2013244. Springer, Heidelberg (2000)"},{"key":"23_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45504-3","volume-title":"Proc. Haskell Workshop 2001","author":"W. Kahl","year":"2001","unstructured":"Kahl, W., Scheffczyk, J.: Named instances for haskell type classes. In: Hinze, R. (ed.) A Comparative Study of Very Large Data Bases. LNCS, vol.\u00a059. Springer, Heidelberg (2001)"},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/3-540-48256-3_11","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Wenzel, M., Paulson, L.C.: Locales - A Sectioning Concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 149\u2013166. Springer, Heidelberg (1999)"},{"key":"23_CR11","unstructured":"Letouzey, P.: Programmation fonctionnelle certifie \u2013 L\u2019extraction de programmes dans l\u2019assistant Coq. PhD thesis, Universit Paris-Sud (July 2004)"},{"key":"23_CR12","unstructured":"Moors, A., Piessens, F., Odersky, M.: Generics of a higher kind. In: ECOOP 2008 (submitted, 2008)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"462","DOI":"10.1007\/3-540-44659-1_29","volume-title":"Theorem Proving in Higher Order Logics","author":"R. Pollack","year":"2000","unstructured":"Pollack, R.: Dependently typed records for representing mathematical structure. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 462\u2013479. Springer, Heidelberg (2000)"},{"key":"23_CR14","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/263699.263742","volume-title":"POPL","author":"A. Sa\u00efbi","year":"1997","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: POPL, La Sorbonne, Paris, France, January 15-17, 1997, pp. 292\u2013301. ACM Press, New York (1997)"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-74464-1_16","volume-title":"Types for Proofs and Programs","author":"M. Sozeau","year":"2007","unstructured":"Sozeau, M.: Subset coercions in Coq. In: Altenkirch, T., McBride, C. (eds.) TYPES 2006. LNCS, vol.\u00a04502, pp. 237\u2013252. Springer, Heidelberg (2007)"},{"key":"23_CR16","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual \u2013 Version V8.1 (July 2006), \n                    \n                      http:\/\/coq.inria.fr"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: POPL, Austin, Texas, pp. 60\u201376 (1989)","DOI":"10.1145\/75277.75283"},{"key":"23_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"},{"key":"23_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/11542384_8","volume-title":"The Seventeen Provers of the World","author":"M. Wenzel","year":"2006","unstructured":"Wenzel, M., Paulson, L.: Isabelle\/isar. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol.\u00a03600, pp. 41\u201349. Springer, Heidelberg (2006)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71067-7_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T11:30:35Z","timestamp":1558265435000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71067-7_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710653","9783540710677"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71067-7_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}