TY - GEN
T1 - The rooster and the butterflies
AU - Mahboubi, Assia
PY - 2013
Y1 - 2013
N2 - This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system. © 2013 Springer-Verlag Berlin Heidelberg.
AB - This paper describes a machine-checked proof of the Jordan-Hölder theorem for finite groups. This purpose of this description is to discuss the representation of the elementary concepts of finite group theory inside type theory. The design choices underlying these representations were crucial to the successful formalization of a complete proof of the Odd Order Theorem with the Coq system. © 2013 Springer-Verlag Berlin Heidelberg.
UR - http://www.scopus.com/inward/record.url?scp=84880744004&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-39320-4_1
DO - 10.1007/978-3-642-39320-4_1
M3 - Conference contribution
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 18
BT - Intelligent Computer Mathematics - MKM, Calculemus, DML, and Systems and Projects 2013 - Held as Part of CICM 2013, Proceedings
T2 - Conference on Intelligent Computer Mathematics, CICM 2013, Co-located with the MKM 2013, Calculemus 2013, DML 2013, and Systems and Projects 2013
Y2 - 8 July 2013 through 12 July 2013
ER -