A Modular Formalisation of Finite Group Theory

Abstract : 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.


https://hal.inria.fr/inria-00139131
Contributeur : Rapport de Recherche Inria <>
Soumis le : mardi 3 avril 2007 - 11:48:23
Dernière modification le : samedi 17 septembre 2016 - 01:36:42
Document(s) archivé(s) le : mardi 21 septembre 2010 - 12:47:34

Fichiers

RR-6156.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00139131, version 2

Collections

Citation

Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. [Research Report] RR-6156, INRIA. 2007, pp.17. <inria-00139131v2>

Exporter

Partager

Métriques

Consultations de
la notice

745

Téléchargements du document

316