Name
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 the 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. |
Year | Venue | Keywords |
|---|---|---|
2007 | TPHOLs | modular formalisation,finite group theory,feit-thompson theorem,elementary group theory,long-term effort,special care,initial base,proof assistant,group theory |
Field | DocType | Volume |
Elementary group,Algebra,Computer science,Theoretical computer science,Type inference,Modular design,Coset,Finite group | Conference | 4732 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-74590-4 | 33 |
PageRank | References | Authors |
1.83 | 8 | 5 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Georges Gonthier | 1 | 2275 | 195.06 |
| Assia Mahboubi | 2 | 308 | 20.84 |
| Laurence Rideau | 3 | 253 | 16.08 |
| Enrico Tassi | 4 | 327 | 21.79 |
| Laurent Théry | 5 | 456 | 41.21 |