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)
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.
- a – Microsoft Research
- b – INRIA Futurs
- c – Università degli studi di Bologna
- 1: Programming Principles and Tools
- 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
- Domain : Computer Science/Logic in Computer Science
Computer Science/Mathematical SoftwareMathematics/Group Theory - Keywords : finite groups – proof assistants – formalisation of mathematics
- Internal note : RR-6156
- Available versions : v1 (2007-03-29) v2 (2007-04-03)
- inria-00139131, version 2
- http://hal.inria.fr/inria-00139131
- oai:hal.inria.fr:inria-00139131
- From: Rapport De Recherche Inria
- Submitted on: Tuesday, 3 April 2007 11:48:23
- Updated on: Wednesday, 15 October 2008 14:19:06
Associated documents
Export