inria-00139131, version 2
A Modular Formalisation of Finite Group Theory
Georges Gonthier
a, 1Assia Mahboubi b, 2Laurence Rideau 3Enrico Tassi c, 4Laurent Théry 3
N° RR-6156 (2007)
Résumé : In this paper, we present a formalisation of elementary group theory done in Coq. This work is the first milestone of a long-term effort to formalise Feit-Thompson theorem. As our further developments will heavily rely on this initial base, we took special care to articulate it in the most compositional way.
- a – Microsoft Research
- b – INRIA Futurs
- c – Università degli studi di Bologna
- 1 : Programming Principles and Tools [Cambridge]
- Microsoft
- 2 : Microsoft Research - Inria Joint Centre (MSR - INRIA)
- INRIA – Microsoft – Microsoft Research Laboratory Cambridge
- 3 : MARELLE (INRIA Sophia Antipolis)
- INRIA
- 4 : Department of Computer Science
- University of Bologna
- Domaine : Informatique/Logique en informatique
Informatique/Logiciel mathématiqueMathématiques/Théorie des groupes - Mots-clés : finite groups – proof assistants – formalisation of mathematics
- Référence interne : RR-6156
- Versions disponibles : v1 (29-03-2007) v2 (03-04-2007)
- inria-00139131, version 2
- http://hal.inria.fr/inria-00139131
- oai:hal.inria.fr:inria-00139131
- Contributeur : Rapport De Recherche Inria
- Soumis le : Mardi 3 Avril 2007, 11:48:23
- Dernière modification le : Mercredi 15 Octobre 2008, 14:19:06
Documents associés
Exporter