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.
Complete list of metadatas

https://hal.inria.fr/inria-00139131
Contributor : Assia Mahboubi <>
Submitted on : Thursday, March 29, 2007 - 2:35:10 PM
Last modification on : Monday, February 12, 2018 - 1:26:02 PM
Long-term archiving on: Wednesday, April 7, 2010 - 12:51:12 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00139131, version 1

Citation

Georges Gonthier, Assia Mahboubi, Laurence Rideau, Enrico Tassi, Laurent Théry. A Modular Formalisation of Finite Group Theory. [Research Report] 2007. ⟨inria-00139131v1⟩

Share

Metrics

Record views

38

Files downloads

98