{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:08:43Z","timestamp":1742800123473},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_35","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"490-493","source":"Crossref","is-referenced-by-count":5,"title":["Developing the Algebraic Hierarchy with Type Classes in Coq"],"prefix":"10.1007","author":[{"given":"Bas","family":"Spitters","sequence":"first","affiliation":[]},{"given":"Eelis","family":"van der Weegen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"35_CR1","first-page":"98","volume-title":"Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Coen, C.S., Tassi, E.: Hints in unification. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, p. 98. Springer, Heidelberg (2009)"},{"key":"35_CR2","series-title":"Lecture Notes in Computer Science","volume-title":"Types for Proofs and Programs","year":"2009","unstructured":"Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.): TYPES 2008. LNCS, vol.\u00a05497. Springer, Heidelberg (2009)"},{"key":"35_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/3-540-48256-3_10","volume-title":"Theorem Proving in Higher Order Logics","author":"V. Capretta","year":"1999","unstructured":"Capretta, V.: Universal algebra in type theory. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Th\u00e9ry, L. (eds.) TPHOLs 1999. LNCS, vol.\u00a01690, pp. 131\u2013148. Springer, Heidelberg (1999)"},{"key":"35_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L. Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-coRN, the constructive coq repository at nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol.\u00a03119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"key":"35_CR5","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-540-85110-3_23","volume-title":"Intelligent Computer Mathematics","author":"C. Dom\u00ednguez","year":"2008","unstructured":"Dom\u00ednguez, C.: Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS (LNAI), vol.\u00a05144, pp. 270\u2013284. Springer, Heidelberg (2008)"},{"key":"35_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"TPHOLs 2009","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"issue":"4","key":"35_CR7","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1006\/jsco.2002.0552","volume":"34","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: A constructive algebraic hierarchy in Coq. J. Symb. Comput.\u00a034(4), 271\u2013286 (2002)","journal-title":"J. Symb. Comput."},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, et al. (eds.) [2], pp. 153\u2013168","DOI":"10.1007\/978-3-642-02444-3_10"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"Luo, Z.: Manifest fields and module mechanisms in intensional type theory. In: Berardi, et al. (eds.) [2], pp. 237\u2013255","DOI":"10.1007\/978-3-642-02444-3_15"},{"issue":"1","key":"35_CR10","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A new look at generalized rewriting in type theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,16]],"date-time":"2019-03-16T06:03:14Z","timestamp":1552716194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}