{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:48:24Z","timestamp":1725490104294},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540745907"},{"type":"electronic","value":"9783540745914"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74591-4_8","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T10:49:52Z","timestamp":1187779792000},"page":"86-101","source":"Crossref","is-referenced-by-count":29,"title":["A Modular Formalisation of Finite Group Theory"],"prefix":"10.1007","author":[{"given":"Georges","family":"Gonthier","sequence":"first","affiliation":[]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","unstructured":"Arthan, R.: Some group theory, available at \n                  \n                    http:\/\/www.lemma-one.com\/ProofPower\/examples\/wrk068.pdf"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"Avigad, J., Donnelly, K., Gray, D., Raff, P.: A Formally Verified Proof of the Prime Number Theorem. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1297658.1297660"},{"key":"8_CR3","unstructured":"Bailey, A.: Representing algebra in LEGO. Master\u2019s thesis, University of Edinburgh (1993)"},{"issue":"2","key":"8_CR4","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":"8_CR5","series-title":"London Mathematical Society Lecture Note Series","volume-title":"Local analysis for the Odd Order Theorem","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":"8_CR6","unstructured":"Constantine, G.M.: Group Theory, available at \n                  \n                    http:\/\/www.pitt.edu\/~gmc\/algsyl.html"},{"issue":"3","key":"8_CR7","doi-asserted-by":"crossref","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":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/3-540-45842-5_7","volume-title":"Types for Proofs and Programs","author":"H. Geuvers","year":"2002","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A Constructive Proof of the Fundamental Theorem of Algebra without Using the Rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol.\u00a02277, pp. 96\u2013111. Springer, Heidelberg (2002)"},{"key":"8_CR9","unstructured":"Gonthier, G.: A computer-checked proof of the four-colour theorem, available at \n                  \n                    http:\/\/research.microsoft.com\/~gonthier\/4colproof.pdf"},{"key":"8_CR10","unstructured":"Gonthier, G.: Notations of the four colour theorem proof, available at \n                  \n                    http:\/\/research.microsoft.com\/~gonthier\/4colnotations.pdf"},{"key":"8_CR11","volume-title":"Introduction to HOL : a theorem proving environment for higher-order logic","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher-order logic. Cambridge University Press, Cambridge (1993)"},{"key":"8_CR12","unstructured":"Gunter, E.: Doing Algebra in Simple Type Theory. Technical Report MS-CIS-89-38, University of Pennsylvania (1989)"},{"issue":"3-4","key":"8_CR13","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1023\/A:1006269330992","volume":"23","author":"F. Kamm\u00fcller","year":"1999","unstructured":"Kamm\u00fcller, F., Paulson, L.C.: A Formal Proof of Sylow\u2019s Theorem. Journal of Automating Reasoning\u00a023(3-4), 235\u2013264 (1999)","journal-title":"Journal of Automating Reasoning"},{"key":"8_CR14","unstructured":"The Coq development team: The Coq proof assistant reference manual. LogiCal Project, Version 8.1 (2007)"},{"key":"8_CR15","unstructured":"The Mizar\u00a0Home Page, \n                  \n                    http:\/\/www.mizar.org\/"},{"key":"8_CR16","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 (December 1996)"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle: a generic theorem prover","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle: a generic theorem prover. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"8_CR18","series-title":"London Mathematical Society Lecture Note Series","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511565861","volume-title":"Character Theory for the Odd Order Theorem","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":"8_CR19","unstructured":"The\u00a0Flyspeck Project, \n                  \n                    http:\/\/www.math.pitt.edu\/~thales\/flyspeck\/"},{"key":"8_CR20","unstructured":"Rideau, L., Th\u00e9ry, L.: Formalising Sylow\u2019s theorems in Coq. Technical Report 0327, INRIA (2006)"},{"key":"8_CR21","unstructured":"Werner, B.: Une th\u00e9orie des Constructions Inductives. PhD thesis, Paris 7 (1994)"},{"key":"8_CR22","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/BF01240818","volume":"10","author":"H. Wielandt","year":"1959","unstructured":"Wielandt, H.: Ein beweis f\u00fcr die Existenz der Sylowgruppen. Archiv der Mathematik\u00a010, 401\u2013402 (1959)","journal-title":"Archiv der Mathematik"},{"issue":"3","key":"8_CR23","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00244488","volume":"6","author":"Y. Yu","year":"1990","unstructured":"Yu, Y.: Computer Proofs in Group Theory. J. Autom. Reasoning\u00a06(3), 251\u2013286 (1990)","journal-title":"J. Autom. Reasoning"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74591-4_8.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:28:14Z","timestamp":1619504894000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74591-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540745907","9783540745914"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74591-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}