{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T00:45:09Z","timestamp":1791420309807,"version":"4.3.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642228629","type":"print"},{"value":"9783642228636","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22863-6_10","type":"book-chapter","created":{"date-parts":[[2011,8,8]],"date-time":"2011-08-08T05:47:55Z","timestamp":1312782475000},"page":"103-118","source":"Crossref","is-referenced-by-count":25,"title":["Point-Free, Set-Free Concrete Linear Algebra"],"prefix":"10.1007","author":[{"given":"Georges","family":"Gonthier","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"10_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":"10_CR2","volume-title":"Finite groups","author":"D. Gorenstein","year":"1980","unstructured":"Gorenstein, D.: Finite groups, 2nd edn. Chelsea, New York (1980)","edition":"2"},{"key":"10_CR3","volume-title":"Local analysis for the Odd Order Theorem. London Mathematical Society Lecture Note Series","author":"H. Bender","year":"1994","unstructured":"Bender, H., Glauberman, G.: Local analysis for the Odd Order Theorem. London Mathematical Society Lecture Note Series, vol.\u00a0188. Cambridge University Press, Cambridge (1994)"},{"key":"10_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511565861","volume-title":"Character Theory for the Odd Order Theorem. London Mathematical Society Lecture Note Series","author":"T. Peterfalvi","year":"2000","unstructured":"Peterfalvi, T.: Character Theory for the Odd Order Theorem. London Mathematical Society Lecture Note Series, vol.\u00a0272. Cambridge University Press, Cambridge (2000)"},{"key":"10_CR5","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":"10_CR6","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":"10_CR7","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)"},{"key":"10_CR8","unstructured":"Pottier, L.: User contributions in Coq, Algebra (1999), http:\/\/coq.inria.fr\/contribs\/Algebra.html"},{"key":"10_CR9","unstructured":"Blanqui, F., Coupet-grimal, S., Delobel, W., Koprowski, A.: Color: a Coq library on rewriting and termination. In: Eighth Int. Workshop on Termination, WST (2006); to appear in MSCS"},{"issue":"1","key":"10_CR10","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":"10_CR11","doi-asserted-by":"crossref","unstructured":"Obua, S.: Proving Bounds for Real Linear Programs in Isabelle\/HOL. Theorem Proving in Higher-Order Logics, 227\u2013244 (2005)","DOI":"10.1007\/11541868_15"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Harrison","year":"2005","unstructured":"Harrison, J.: A HOL Theory of Euclidian Space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 114\u2013129. Springer, Heidelberg (2005)"},{"key":"10_CR13","unstructured":"Cowles, J., Gamboa, R., Baalen, J.V.: Using ACL2 Arrays to Formalize Matrix Algebra. In: ACL2 Workshop (2003)"},{"key":"10_CR14","unstructured":"Stein, J.: Documentation for the formalization of Linerar Agebra, http:\/\/www.cs.ru.nl\/~jasper\/"},{"key":"10_CR15","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, version 8.3 (2010)"},{"key":"10_CR16","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. INRIA Technical report, http:\/\/hal.inria.fr\/inria-00258384"},{"key":"10_CR17","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":"2","key":"10_CR18","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"}],"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-22863-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T18:13:39Z","timestamp":1560449619000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22863-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642228629","9783642228636"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22863-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}