{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:45:58Z","timestamp":1767926758741,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642396335","type":"print"},{"value":"9783642396342","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39634-2_5","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T13:52:36Z","timestamp":1374501156000},"page":"19-34","source":"Crossref","is-referenced-by-count":26,"title":["Canonical Structures for the Working Coq User"],"prefix":"10.1007","author":[{"given":"Assia","family":"Mahboubi","sequence":"first","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Sacerdoti Coen, C., Tassi, E.: Hints in unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"5_CR3","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first order theory. PhD thesis, \u00c9cole polytechnique (2012)"},{"key":"5_CR4","unstructured":"Garillot, F.: Generic Proof Tools and Finite Group Theory. PhD thesis, \u00c9cole polytechnique (2011)"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","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":"5_CR6","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":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-22863-6_10","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-free, set-free concrete linear algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 103\u2013118. Springer, Heidelberg (2011)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Th\u00e9ry, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"5_CR9","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2012)"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: How to make ad hoc proof automation less ad hoc. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) ICFP, pp. 163\u2013175. ACM (2011)","DOI":"10.1145\/2034574.2034798"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Hinze, R.: Fun with phantom types. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming, Cornerstones of Computing, pp. 245\u2013262 (2003)","DOI":"10.1007\/978-1-349-91518-7_12"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Huet, G.P., Sa\u00efbi, A.: Constructive category theory. In: Plotkin, G.D., Stirling, C., Tofte, M. (eds.) Proof, Language, and Interaction, pp. 239\u2013276. The MIT Press (2000)","DOI":"10.7551\/mitpress\/5641.003.0015"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Sa\u00efbi, A.: Typing algorithm in type theory with inheritance. In: Lee, P., Henglein, F., Jones, N.D. (eds.) POPL, pp. 292\u2013301. ACM Press (1997)","DOI":"10.1145\/263699.263742"},{"key":"5_CR14","unstructured":"Sa\u00efbi, A.: Outils G\u00e9n\u00e9riques de Mod\u00e9lisation et de D\u00e9monstration pour la Formalisation des Math\u00e9matiques en Th\u00e9orie des Types: application \u00e0 la Th\u00e9orie des Cat\u00e9gories. PhD thesis, Universit\u00e9 Paris VI (1999)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"issue":"4","key":"5_CR16","doi-asserted-by":"publisher","first-page":"795","DOI":"10.1017\/S0960129511000119","volume":"21","author":"B. Spitters","year":"2011","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science\u00a021(4), 795\u2013825 (2011)","journal-title":"Mathematical Structures in Computer Science"},{"key":"5_CR17","unstructured":"The Coq Development Team. The Coq proof assistant, version 8.4., http:\/\/coq.inria.fr"},{"key":"5_CR18","unstructured":"The Mathematical Component Team. A Formalization of the Odd Order Theorem using the Coq proof assistant (September 2012), http:\/\/www.msr-inria.inria.fr\/Projects\/math-components\/feit-thompson"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of POPL, pp. 60\u201376. ACM (1989)","DOI":"10.1145\/75277.75283"}],"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-39634-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,15]],"date-time":"2024-05-15T05:16:33Z","timestamp":1715750193000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39634-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642396335","9783642396342"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39634-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}