{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,8]],"date-time":"2025-05-08T23:04:37Z","timestamp":1746745477686},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642393198"},{"type":"electronic","value":"9783642393204"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39320-4_1","type":"book-chapter","created":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T11:22:52Z","timestamp":1372677772000},"page":"1-18","source":"Crossref","is-referenced-by-count":1,"title":["The Rooster and the Butterflies"],"prefix":"10.1007","author":[{"given":"Assia","family":"Mahboubi","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"The Coq Proof Assistant, http:\/\/coq.inria.fr"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Aschbacher, M.: Finite Group Theory. Cambridge Studies in Advanced Mathematics. Cambridge University Press (2000)","DOI":"10.1017\/CBO9781139175319"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bender, H., Glauberman, G.: Local analysis for the Odd Order Theorem. London Mathematical Society, LNS, vol.\u00a0188. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511665592"},{"key":"1_CR4","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, Berlin (2004)"},{"key":"1_CR5","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":"1_CR6","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Symposium on Automatic Demonstration","author":"N.G. Bruijn de","year":"1970","unstructured":"de Bruijn, N.G.: The mathematical language AUTOMATH, its usage, and some of its extensions. In: Laudet, M., Lacombe, D., Nolin, L., Sch\u00fctzenberger, M. (eds.) Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol.\u00a0125, pp. 29\u201361. Springer, Heidelberg (1970)"},{"issue":"3","key":"1_CR7","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":"1_CR8","unstructured":"Garillot, F.: Generic Proof Tools and Finite Group Theory. PhD thesis, \u00c9cole polytechnique (2011)"},{"key":"1_CR9","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":"1_CR10","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O\u2019Connor, R., Biha, S.O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. To appear in the Proceedings of the ITP 2013 Conference (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"issue":"2","key":"1_CR11","first-page":"95","volume":"3","author":"G. Gonthier","year":"2010","unstructured":"Gonthier, G., Mahboubi, A.: An introduction to small scale reflection in Coq. Journal of Formalized Reasoning\u00a03(2), 95\u2013152 (2010)","journal-title":"Journal of Formalized Reasoning"},{"key":"1_CR12","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":"1_CR13","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Rapport de recherche RR-6455, INRIA (2012)"},{"issue":"4","key":"1_CR14","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1017\/S0956796898003153","volume":"8","author":"M. Hedberg","year":"1998","unstructured":"Hedberg, M.: A coherence theorem for Martin-L\u00f6f\u2019s type theory. Journal of Functional Programming\u00a08(4), 413\u2013436 (1998)","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"1_CR15","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/BF01446791","volume":"34","author":"O. H\u00f6lder","year":"1889","unstructured":"H\u00f6lder, O.: Zur\u00fcckf\u00fchrung einer beliebigen algebraischen Gleichung auf eine Kette von Gleichungen. Mathematische Annalen\u00a034(1), 26\u201356 (1889)","journal-title":"Mathematische Annalen"},{"key":"1_CR16","unstructured":"Isaacs, I.: Character Theory of Finite Groups. AMS Chelsea Pub. Series (1976)"},{"key":"1_CR17","unstructured":"Jordan, C.: Trait\u00e9 des substitutions et des \u00e9quations alg\u00e9briques. Gauthier-Villars, Paris (1870)"},{"key":"1_CR18","unstructured":"Kurzweil, H., Stellmacher, B.: The Theory of Finite Groups: An Introduction. Universitext Series. Springer (2010)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Mahboubi, A., Tassi, E.: Canonical structures for the working coq user. To appear in the Proceedings of the ITP 2013 Conference (2013)","DOI":"10.1007\/978-3-642-39634-2_5"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Peterfalvi, T.: Character Theory for the Odd Order Theorem. London Mathematical Society, LNS, vol.\u00a0272. Cambridge University Press (2000)","DOI":"10.1017\/CBO9780511565861"},{"key":"1_CR21","unstructured":"The Univalent Foundations Program. Homotopy type theory: Univalent foundations of mathematics. Technical report, Institute for Advanced Study (2013)"},{"key":"1_CR22","unstructured":"Wiedijk, F.: The \u201cde Bruijn factor\u201d, http:\/\/www.cs.ru.nl\/~freek\/factor\/"},{"issue":"1","key":"1_CR23","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1007\/BF02940667","volume":"10","author":"H. Zassenhaus","year":"1934","unstructured":"Zassenhaus, H.: Zum satz von Jordan-H\u00f6lder-Schreier. Abhandlungen aus dem Mathematischen Seminar der Universit\u00e4t Hamburg\u00a010(1), 106\u2013108 (1934)","journal-title":"Abhandlungen aus dem Mathematischen Seminar der Universit\u00e4t Hamburg"}],"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-39320-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,16]],"date-time":"2019-07-16T20:41:10Z","timestamp":1563309670000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39320-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642393198","9783642393204"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39320-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}