The Rooster and the Butterflies

Abstract : 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.
Type de document :
Communication dans un congrès
Jacques Carette and David Aspinal and Christopher Lange and Petr Sojka and Wolfgang Windsteiger. CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. Springer, 7961, pp.1-18, 2013, Lecture Notes in Artificial Intelligence. <10.1007/978-3-642-39320-4_1>
Liste complète des métadonnées


https://hal.inria.fr/hal-00825074
Contributeur : Assia Mahboubi <>
Soumis le : lundi 15 juillet 2013 - 21:31:51
Dernière modification le : jeudi 9 février 2017 - 15:48:06
Document(s) archivé(s) le : mercredi 5 avril 2017 - 12:20:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Assia Mahboubi. The Rooster and the Butterflies. Jacques Carette and David Aspinal and Christopher Lange and Petr Sojka and Wolfgang Windsteiger. CICM 2013 - Conference on Intelligent Computer Mathematics - 2013, Jul 2013, Bath, United Kingdom. Springer, 7961, pp.1-18, 2013, Lecture Notes in Artificial Intelligence. <10.1007/978-3-642-39320-4_1>. <hal-00825074v3>

Partager

Métriques

Consultations de
la notice

391

Téléchargements du document

293