{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T10:57:15Z","timestamp":1725533835738},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642026133"},{"type":"electronic","value":"9783642026140"}],"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-02614-0_34","type":"book-chapter","created":{"date-parts":[[2009,7,2]],"date-time":"2009-07-02T07:47:24Z","timestamp":1246520844000},"page":"438-452","source":"Crossref","is-referenced-by-count":1,"title":["Finite Groups Representation Theory with Coq"],"prefix":"10.1007","author":[{"given":"Sidi Ould","family":"Biha","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","unstructured":"Gonthier, G.: Formal proof - The Four-Color Theorem. Notices of the American Mathematical Society\u00a055(11) (2008)"},{"key":"34_CR2","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A formally verified proof of the prime number theorem. CoRR abs\/cs\/0509025 (2005)"},{"key":"34_CR3","unstructured":"The\u00a0Flyspeck project, http:\/\/code.google.com\/p\/flyspeck\/"},{"key":"34_CR4","unstructured":"The C-CoRN project, http:\/\/c-corn.cs.ru.nl\/"},{"key":"34_CR5","unstructured":"Stephen, W.: The Mathematica Book, 5th edn. Wolfram Media (2003)"},{"key":"34_CR6","unstructured":"The GAP\u00a0Group: GAP \u2013 Groups, Algorithms, and Programming, Version 4.4.12 (2008)"},{"key":"34_CR7","unstructured":"Mathematical\u00a0Components manifesto: http:\/\/www.msr-inria.inria.fr\/Projects\/math-components\/manifesto"},{"issue":"3","key":"34_CR8","doi-asserted-by":"publisher","first-page":"775","DOI":"10.2140\/pjm.1963.13.775","volume":"13","author":"W. Feit","year":"1963","unstructured":"Feit, W., Thompson, J.G.: Solvability of groups of odd order. Pacific Journal of Mathematics\u00a013(3), 775\u20131029 (1963)","journal-title":"Pacific Journal of Mathematics"},{"key":"34_CR9","unstructured":"Gonthier, G., Mahboubi, A.: A small scale reflection extension for the Coq system. INRIA Technical report, http:\/\/hal.inria.fr\/inria-00258384"},{"key":"34_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art: the Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"key":"34_CR11","unstructured":"Coq development team: The Coq Proof Assistant Reference Manual, version 8.2 (2009)"},{"key":"34_CR12","doi-asserted-by":"crossref","unstructured":"Gelbart, S.: An Elementary Introduction to the Langlands Program. Bulletin of the American Mathematical Society\u00a010(2) (1984)","DOI":"10.1090\/S0273-0979-1984-15237-6"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Isaacs, I.M.: Character Theory of Finite Groups. American Mathematical Society (1994)","DOI":"10.1017\/S1446788700036077"},{"key":"34_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511814532","volume-title":"Representations and Characters of Groups","author":"G. James","year":"2001","unstructured":"James, G., Liebeck, M.: Representations and Characters of Groups. Cambridge University Press, Cambridge (2001)"},{"key":"34_CR15","unstructured":"Webb, P.: Finite Group Representations for the Pure Mathematician. The manuscript of the book is available on the author web page, http:\/\/www.math.umn.edu\/~webb\/RepBook\/index.html"},{"key":"34_CR16","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":"34_CR17","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., Biha, S.O., 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":"34_CR18","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)"},{"issue":"4","key":"34_CR19","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":"34_CR20","unstructured":"Pottier, L.: User contributions in Coq, Algebra (1999), http:\/\/coq.inria.fr\/contribs\/Algebra.html"},{"issue":"2","key":"34_CR21","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":"34_CR22","unstructured":"Mizar\u00a0Mathematical Library, http:\/\/mizar.org\/library\/"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02614-0_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T01:40:56Z","timestamp":1558402856000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02614-0_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642026133","9783642026140"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02614-0_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}