{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:47:08Z","timestamp":1767926828910,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642033582","type":"print"},{"value":"9783642033599","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_23","type":"book-chapter","created":{"date-parts":[[2009,8,19]],"date-time":"2009-08-19T21:46:12Z","timestamp":1250718372000},"page":"327-342","source":"Crossref","is-referenced-by-count":80,"title":["Packaging Mathematical Structures"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Garillot","sequence":"first","affiliation":[]},{"given":"Georges","family":"Gonthier","sequence":"additional","affiliation":[]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"23_CR1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4613-0041-0","volume-title":"Algebra","author":"S. Lang","year":"2002","unstructured":"Lang, S.: Algebra. Springer, Heidelberg (2002)"},{"key":"23_CR2","unstructured":"Jackson, P.: Enhancing the Nuprl proof-development system and applying it to computational abstract algebra. PhD thesis, Cornell University (1995)"},{"key":"23_CR3","unstructured":"Betarte, G., Tasistro, A.: Formalisation of systems of algebras using dependent record types and subtyping: An example. In: Proc. 7th Nordic workshop on Programming Theory (1995)"},{"key":"23_CR4","unstructured":"Pottier, L.: User contributions in Coq, Algebra (1999), \n                    \n                      http:\/\/coq.inria.fr\/contribs\/Algebra.html"},{"issue":"4","key":"23_CR5","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. Journal of Symbolic Computation\u00a034(4), 271\u2013286 (2002)","journal-title":"Journal of Symbolic Computation"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/978-3-642-02444-3_10","volume-title":"TYPES 2008","author":"F. Haftmann","year":"2009","unstructured":"Haftmann, F., Wenzel, M.: Local theory specifications in Isabelle\/Isar. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol.\u00a05497, pp. 153\u2013168. Springer, Heidelberg (2009)"},{"issue":"1","key":"23_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/jsco.2001.0456","volume":"32","author":"P. Rudnicki","year":"2001","unstructured":"Rudnicki, P., Schwarzweller, C., Trybulec, A.: Commutative algebra in the Mizar system. J. Symb. Comput.\u00a032(1), 143\u2013169 (2001)","journal-title":"J. Symb. Comput."},{"key":"23_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":"23_CR9","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":"23_CR10","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. INRIA Technical report, \n                    \n                      http:\/\/hal.inria.fr\/inria-00258384"},{"key":"23_CR11","unstructured":"Paulin-Mohring, C.: D\u00e9finitions Inductives en Th\u00e9orie des Types d\u2019Ordre Sup\u00e9rieur. Habilitation \u00e0 diriger les recherches, Universit\u00e9 Claude Bernard Lyon I (1996)"},{"key":"23_CR12","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)"},{"key":"23_CR13","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/s001650200018","volume":"13","author":"R. Pollack","year":"2002","unstructured":"Pollack, R.: Dependently typed records in type theory. Formal Aspects of Computing\u00a013, 386\u2013402 (2002)","journal-title":"Formal Aspects of Computing"},{"key":"23_CR14","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N.G.D. Bruijn","year":"1991","unstructured":"Bruijn, N.G.D.: Telescopic mappings in typed lambda calculus. Information and Computation\u00a091, 189\u2013204 (1991)","journal-title":"Information and Computation"},{"issue":"4","key":"23_CR15","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1145\/1183278.1183280","volume":"7","author":"L.C. Paulson","year":"2006","unstructured":"Paulson, L.C.: Defining Functions on Equivalence Classes. ACM Transactions on Computational Logic\u00a07(4), 658\u2013675 (2006)","journal-title":"ACM Transactions on Computational Logic"},{"issue":"2","key":"23_CR16","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1017\/S0956796802004501","volume":"13","author":"G. Barthe","year":"2003","unstructured":"Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. Journal of Functional Programming\u00a013(2), 261\u2013293 (2003)","journal-title":"Journal of Functional Programming"},{"key":"23_CR17","first-page":"57","volume-title":"Proceedings of the PLPV 2007 workshop","author":"T. Altenkirch","year":"2007","unstructured":"Altenkirch, T., McBride, C., Swierstra, W.: Observational equality, now! In: Proceedings of the PLPV 2007 workshop, pp. 57\u201368. ACM, New York (2007)"},{"issue":"258","key":"23_CR18","doi-asserted-by":"publisher","first-page":"1073","DOI":"10.1090\/S0025-5718-07-01957-6","volume":"76","author":"G. Olteanu","year":"2007","unstructured":"Olteanu, G.: Computing the Wedderburn decomposition of group algebras by the Brauer-Witt theorem. Mathematics of Computation\u00a076(258), 1073\u20131087 (2007)","journal-title":"Mathematics of Computation"},{"key":"23_CR19","volume-title":"An Introduction to the Theory of Groups","author":"J.J. Rotman","year":"1994","unstructured":"Rotman, J.J.: An Introduction to the Theory of Groups. Springer, Heidelberg (1994)"},{"key":"23_CR20","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"2003","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 2nd edn. McGraw-Hill, New York (2003)","edition":"2"},{"key":"23_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-68103-8_11","volume-title":"Types for Proofs and Programs","author":"C. Sacerdoti Coen","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: Working with Mathematical Structures in Type Theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 157\u2013172. Springer, Heidelberg (2008)"},{"key":"23_CR22","first-page":"51","volume":"1","author":"C. Sacerdoti Coen","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: A constructive and formal proof of Lebesgue Dominated Convergence Theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning\u00a01, 51\u201389 (2008)","journal-title":"Journal of Formalized Reasoning"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T08:24:42Z","timestamp":1552119882000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}