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
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, April 3, 2007 - 11:48:23 AM
Last modification on : Wednesday, October 15, 2008 - 2:19:06 PM

Files

RR-6156.pdf
fileSource_public_author

Identifiers

  • 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, 2007, pp.17. <inria-00139131v2>

Export

Share

Metrics

Consultation de
la notice

504

Téléchargement du document

196